diff options
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 7b28895814..5ff3032ec4 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -22,7 +22,6 @@ open Nameops open Constrexpr open Constrexpr_ops open Constrintern -open Nametab open Impargs open Reductionops open Indtypes @@ -103,10 +102,6 @@ let mk_mltype_data sigma env assums arity indname = let is_ml_type = is_sort env sigma arity in (is_ml_type,indname,assums) -let prepare_param = function - | LocalAssum (na,t) -> Name.get_id na, LocalAssumEntry t - | LocalDef (na,b,_) -> Name.get_id na, LocalDefEntry b - (** Make the arity conclusion flexible to avoid generating an upper bound universe now, only if the universe does not appear anywhere else. This is really a hack to stay compatible with the semantics of template polymorphic @@ -464,7 +459,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not in (* Build the mutual inductive entry *) let mind_ent = - { mind_entry_params = List.map prepare_param ctx_params; + { mind_entry_params = ctx_params; mind_entry_record = None; mind_entry_finite = finite; mind_entry_inds = entries; @@ -575,6 +570,6 @@ let do_mutual_inductive ~template udecl indl cum poly prv ~uniform finite = (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes; + List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false poly) coes; (* If positivity is assumed declares itself as unsafe. *) if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () |