diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-26 21:15:36 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-09-25 10:40:10 +0200 |
| commit | e0547f9e9134a9fff122df900942a094c53535c3 (patch) | |
| tree | 9b5a11a7fb28857dd26f472d6329e14a1529393a /stm | |
| parent | 576d7a815174106f337fca2f19ad7f26a7e87cc4 (diff) | |
Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming guardedness.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/texmacspp.ml | 4 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 4cc362dda..4f014be2d 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -598,14 +598,14 @@ let rec tmpp v loc = (fun (ie, dnl) -> (pp_inductive_expr ie) @ (List.map pp_decl_notation dnl)) iednll) in xmlInductive kind loc exprs - | VernacFixpoint (_, fednll) -> + | VernacFixpoint (_,_, fednll) -> let exprs = List.flatten (* should probably not be flattened *) (List.map (fun (fe, dnl) -> (pp_fixpoint_expr fe) @ (List.map pp_decl_notation dnl)) fednll) in xmlFixpoint exprs - | VernacCoFixpoint (_, cfednll) -> + | VernacCoFixpoint (_,_, cfednll) -> (* Nota: it is like VernacFixpoint without so could be merged *) let exprs = List.flatten (* should probably not be flattened *) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 03ade646b..574cc0044 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -125,14 +125,14 @@ let rec classify_vernac e = CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater - | VernacFixpoint (_,l) -> + | VernacFixpoint (_,_,l) -> let ids, open_proof = List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater else VtSideff ids, VtLater - | VernacCoFixpoint (_,l) -> + | VernacCoFixpoint (_,_,l) -> let ids, open_proof = List.fold_left (fun (l,b) (((_,id),_,_,p),_) -> id::l, b || p = None) ([],false) l in |