Skip to content

Commit

Permalink
fix disappearing fingerprints
Browse files Browse the repository at this point in the history
Signed-off-by: Damien Doligez <[email protected]>
  • Loading branch information
damiendoligez committed Jun 6, 2023
1 parent 581ebd8 commit d080a44
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/module/m_parser.ml
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ let rec modunit = lazy begin
[ Theorem (nm, { bod with active = with_meth bod.active meth }, 0, prf, prf, empty_summary) ]) ;

enabled (punct "----" <*> kwd "MODULE")
>*> use parse <$> (fun m -> [ Submod m ]) ;
>*> use parse <$> (fun m -> m.core.important <- true; [ Submod m ]) ;

punct "----" <!> [] ;
]
Expand Down Expand Up @@ -99,7 +99,7 @@ and parse_ = lazy begin
; extendees = extends
; instancees = []
; defdepth = 0
; important = (* false *) true (* to simplify proofs of submodules *)
; important = false
; body = List.concat mus
; stage = Parsed }
end
Expand Down

0 comments on commit d080a44

Please sign in to comment.