diff options
| author | Pierre-Marie Pédrot | 2016-06-18 20:07:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-18 20:07:02 +0200 |
| commit | b2495b2326083776f9b15355acac77cde73545e1 (patch) | |
| tree | d030b2e5fbd6fe9c7bba68e5fb80d2546ab96f92 /plugins | |
| parent | 561dbba4ce47aa1920b27a6fa3ea1fdb03835557 (diff) | |
| parent | 371d69b334837c51d0dc998ddefbd072ac8dde2f (diff) | |
Merge PR# 169: Local type-in-type flag.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index f69c4d8217..c424fe1226 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1432,7 +1432,7 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.do_mutual_inductive true rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite + with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 8b3d3dc20f..0cacb003d8 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -400,7 +400,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint ~flags:Declareops.safe_flags Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index a78eb1af76..99a165044c 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -887,7 +887,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,pl,impls = Command.interp_mutual_inductive true indl [] + let mie,pl,impls = Command.interp_mutual_inductive 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 pl impls) |