diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/class.ml | 3 | ||||
| -rw-r--r-- | vernac/command.ml | 7 | ||||
| -rw-r--r-- | vernac/indschemes.ml | 2 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 4 | ||||
| -rw-r--r-- | vernac/obligations.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
6 files changed, 11 insertions, 9 deletions
diff --git a/vernac/class.ml b/vernac/class.ml index be682977e..3915148a0 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -222,9 +222,10 @@ let build_id_coercion idf_opt source poly = Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in + let univs = (snd (Evd.universe_context ~names:[] ~extensible:true sigma)) in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - (definition_entry ~types:typ_f ~poly ~univs:(snd (Evd.universe_context sigma)) + (definition_entry ~types:typ_f ~poly ~univs ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in let decl = (constr_entry, IsDefinition IdentityCoercion) in diff --git a/vernac/command.ml b/vernac/command.ml index 15dacb776..59f59e530 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -1019,15 +1019,16 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let binders_rel = nf_evar_context !evdref binders_rel in let binders = nf_evar_context !evdref binders in let top_arity = Evarutil.nf_evar !evdref top_arity in - let pl = Option.map (fun d -> d.univdecl_instance) pl in - let hook, recname, typ = + let pl, plext = Option.cata + (fun d -> d.univdecl_instance, d.univdecl_extensible_instance) ([],true) pl in + let hook, recname, typ = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in let hook l gr _ = let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ty = EConstr.Unsafe.to_constr ty in - let pl, univs = Evd.universe_context ?names:pl !evdref in + let pl, univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in (*FIXME poly? *) let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in (** FIXME: include locality *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index facebd096..90168843a 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -108,7 +108,7 @@ let _ = let define id internal ctx c t = let f = declare_constant ~internal in - let _, univs = Evd.universe_context ctx in + let _, univs = Evd.universe_context ~names:[] ~extensible:true ctx in let univs = if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs else Monomorphic_const_entry univs diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 793022377..391e78bcd 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -49,7 +49,7 @@ let retrieve_first_recthm uctx = function (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - let (_, uctx) = UState.universe_context uctx in + let (_, uctx) = UState.universe_context ~names:[] ~extensible:true uctx in let inst = Univ.UContext.instance uctx in let map (c, ctx) = Vars.subst_instance_constr inst c in (Option.map map (Global.body_of_constant_body cb), is_opaque cb) @@ -450,7 +450,7 @@ let start_proof_com ?inference_hook kind thms hook = let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in let () = if not decl.Misctypes.univdecl_extensible_instance then - ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance) + ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance ~extensible:false) else () in let evd = diff --git a/vernac/obligations.ml b/vernac/obligations.ml index c71feb52b..89b18d254 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -888,7 +888,7 @@ in let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in Univ.Instance.empty, Evd.evar_universe_context ctx' else - let (_, uctx) = UState.universe_context ctx' in + let (_, uctx) = UState.universe_context ~names:[] ~extensible:true ctx' in Univ.UContext.instance uctx, ctx' in let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4fd08b42d..c90d038f6 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1556,7 +1556,7 @@ let vernac_check_may_eval ?loc redexp glopt rc = let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in Evarconv.check_problems_are_solved env sigma'; let sigma',nf = Evarutil.nf_evars_and_universes sigma' in - let pl, uctx = Evd.universe_context sigma' in + let pl, uctx = Evd.universe_context ~names:[] ~extensible:true sigma' in let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in let c = nf c in let j = |