diff options
| author | Arnaud Spiwack | 2015-06-23 17:45:04 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-06-24 17:55:47 +0200 |
| commit | 2adff76c5466734c633923e768c9dcbdc6f28c86 (patch) | |
| tree | aca997d04a076e09ce62929415cd66820a5c92d3 /toplevel/command.ml | |
| parent | 4a73e6b2bfb75451bcda7c74cf7478726a459799 (diff) | |
Add corresponding field in `VernacInductive`.
Makes sure not to generate inductive schemes of assumed positive types.
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 49bd37c697..ca925d4904 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -475,7 +475,7 @@ let check_param = function | LocalRawAssum (nas, Default _, _) -> List.iter check_named nas | LocalRawAssum (nas, Generalized _, _) -> () -let interp_mutual_inductive (paramsl,indl) notations poly prv finite = +let interp_mutual_inductive chk (paramsl,indl) notations poly prv finite = check_all_names_different indl; List.iter check_param paramsl; let env0 = Global.env() in @@ -554,7 +554,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; mind_entry_universes = Evd.universe_context evd; - mind_entry_check_positivity = true; }, + mind_entry_check_positivity = chk; }, impls (* Very syntactical equality *) @@ -636,10 +636,10 @@ type one_inductive_impls = Impargs.manual_explicitation list (* for inds *)* Impargs.manual_explicitation list list (* for constrs *) -let do_mutual_inductive indl poly prv finite = +let do_mutual_inductive chk indl poly prv finite = let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) - let mie,impls = interp_mutual_inductive indl ntns poly prv finite in + let mie,impls = interp_mutual_inductive chk indl ntns poly prv finite in (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie impls); (* Declare the possible notations of inductive types *) |