From 2adff76c5466734c633923e768c9dcbdc6f28c86 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 23 Jun 2015 17:45:04 +0200 Subject: Add corresponding field in `VernacInductive`. Makes sure not to generate inductive schemes of assumed positive types. --- stm/texmacspp.ml | 2 +- stm/vernac_classifier.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 9edc1f1c70..4cc362ddab 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -580,7 +580,7 @@ let rec tmpp v loc = let l = match l with Some x -> x | None -> Decl_kinds.Global in let kind = string_of_assumption_kind l a many in xmlAssumption kind loc exprs - | VernacInductive (_, _, iednll) -> + | VernacInductive (_,_, _, iednll) -> let kind = let (_, _, _, k, _),_ = List.hd iednll in begin diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 2b5eb86834..03ade646b2 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -144,7 +144,7 @@ let rec classify_vernac e = let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in VtSideff ids, VtLater | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater - | VernacInductive (_,_,l) -> + | VernacInductive (_,_,_,l) -> let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ -- cgit v1.2.3 From e0547f9e9134a9fff122df900942a094c53535c3 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 26 Jun 2015 21:15:36 +0200 Subject: Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming guardedness. --- stm/texmacspp.ml | 4 ++-- stm/vernac_classifier.ml | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'stm') diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 4cc362ddab..4f014be2de 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 03ade646b2..574cc0044c 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 -- cgit v1.2.3 From 4d239ab9f096843dc1c78744dfc9b316ab49d6d9 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 15 Jun 2016 19:19:58 +0200 Subject: Allow `Pretyping.search_guard` to not check guard This is a minimal modification to the pretyping interface which allows for toplevel fixed points to be accepted by the pretyper. Toplevel co-fixed points are accepted without this. However (co-)fixed point _nested_ inside a `Definition` or a `Fixpoint` are always checked for guardedness by the pretyper. --- stm/lemmas.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index c766f3fab3..1d591e1be8 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -76,7 +76,7 @@ let adjust_guardness_conditions const = function List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) env (Declareops.uniquize_side_effects eff) in let indexes = - search_guard Loc.ghost env + search_guard ~tflags:{Declarations.check_guarded=true} Loc.ghost env possible_indexes fixdecls in (mkFix ((indexes,0),fixdecls), ctx), eff | _ -> (body, ctx), eff) } -- cgit v1.2.3 From dcf4d3e28813e09fc71f974b79ddf42d2e525976 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 5 Jun 2016 21:50:22 +0200 Subject: Remove the syntax changes introduced by this branch. We decided to only export the API, so that an external plugin can provide this feature without having to merge it in current Coq trunk. This postpones the attribute implementation in vernacular commands after 8.6. --- stm/texmacspp.ml | 6 +++--- stm/vernac_classifier.ml | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) (limited to 'stm') diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 4f014be2de..9edc1f1c70 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -580,7 +580,7 @@ let rec tmpp v loc = let l = match l with Some x -> x | None -> Decl_kinds.Global in let kind = string_of_assumption_kind l a many in xmlAssumption kind loc exprs - | VernacInductive (_,_, _, iednll) -> + | VernacInductive (_, _, iednll) -> let kind = let (_, _, _, k, _),_ = List.hd iednll in begin @@ -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 574cc0044c..2b5eb86834 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 @@ -144,7 +144,7 @@ let rec classify_vernac e = let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in VtSideff ids, VtLater | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater - | VernacInductive (_,_,_,l) -> + | VernacInductive (_,_,l) -> let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ -- cgit v1.2.3