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. --- plugins/funind/glob_term_to_relation.ml | 6 +++--- plugins/funind/merge.ml | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 065c12a2d7..b4febba668 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1424,7 +1424,7 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite + with_full_print (Flags.silently (Command.do_mutual_inductive true rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in @@ -1435,7 +1435,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1450,7 +1450,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ Errors.print reraise in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index ea699580b9..8c4bd484f5 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -884,7 +884,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,impls = Command.interp_mutual_inductive indl [] + let mie,impls = Command.interp_mutual_inductive true indl [] false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) ignore (Command.declare_mutual_inductive_with_eliminations mie impls) -- 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. --- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/indfun.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 61f03d6f22..53ec304ccc 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -166,7 +166,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(None, List.map snd recsl)) + (Vernacexpr.VernacFixpoint(true,None, List.map snd recsl)) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 5dcb0c0439..5c849ba415 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -399,7 +399,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + Command.do_fixpoint ~chkguard:true Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) (((_,fname),_,_,_,_),_) -> -- cgit v1.2.3 From d4f3a1a807d474050a4e91e16ff7813f1db7f537 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 7 Jun 2016 09:52:43 +0200 Subject: Assume totality: dedicated type rather than bool The rational is that 1. further typing flags may be available in the future 2. it makes it easier to trace and document the argument --- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/indfun.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 53ec304ccc..91fcb3f8b9 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -166,7 +166,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(true,None, List.map snd recsl)) + (Vernacexpr.VernacFixpoint({Declarations.check_guarded=true},None, List.map snd recsl)) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 5c849ba415..0ea90ecd12 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -399,7 +399,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint ~chkguard:true Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + Command.do_fixpoint ~flags:{Declarations.check_guarded=true} Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) (((_,fname),_,_,_,_),_) -> -- 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. --- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/glob_term_to_relation.ml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 91fcb3f8b9..61f03d6f22 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -166,7 +166,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint({Declarations.check_guarded=true},None, List.map snd recsl)) + (Vernacexpr.VernacFixpoint(None, List.map snd recsl)) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index b4febba668..f1c379ecc6 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1435,7 +1435,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1450,7 +1450,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ Errors.print reraise in -- cgit v1.2.3