diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-12 17:57:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 18:19:09 +0200 |
| commit | a59bdc4144476c0794ff24fc6180e21671842395 (patch) | |
| tree | ee175002ae8197c9a94e5ec3fcdaeeededbb4f04 /vernac/lemmas.ml | |
| parent | f2a01d400c92c48caf79771f17820a492f99057b (diff) | |
Removing the uses of abstraction-breaking code in Lemmas.
I had to slightly tweak a test in order to work around a bug of simpl that
loses universes constraints when refolding polymorphic fixpoints.
Diffstat (limited to 'vernac/lemmas.ml')
| -rw-r--r-- | vernac/lemmas.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index cfd489dde..645320c60 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -44,12 +44,14 @@ let call_hook fix_exn hook l c = (* Support for mutually proved theorems *) -let retrieve_first_recthm = function +let retrieve_first_recthm uctx = function | VarRef id -> (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - let map (c, ctx) = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in + let (_, uctx) = UState.universe_context 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) | _ -> assert false @@ -413,7 +415,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = let other_thms_data = if List.is_empty other_thms then [] else (* there are several theorems defined mutually *) - let body,opaq = retrieve_first_recthm ref in + let body,opaq = retrieve_first_recthm ctx ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in let ctx = UState.context_set (*FIXME*) ctx in |