diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-09 14:00:42 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2017-09-19 10:28:03 +0200 |
| commit | cd29948855c2cbd3f4065170e41f8dbe625e1921 (patch) | |
| tree | e747c92a12074f2d0753b902c5fe00261d0a0fe4 /vernac/lemmas.ml | |
| parent | c2b881aae9c71a34199d2c66282512f2bdb19cf6 (diff) | |
Don't lose names in UState.universe_context.
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
Diffstat (limited to 'vernac/lemmas.ml')
| -rw-r--r-- | vernac/lemmas.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 = |