diff options
| author | Pierre-Marie Pédrot | 2017-07-12 17:57:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-13 18:19:09 +0200 |
| commit | a59bdc4144476c0794ff24fc6180e21671842395 (patch) | |
| tree | ee175002ae8197c9a94e5ec3fcdaeeededbb4f04 | |
| 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.
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_123.v | 6 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 8 |
2 files changed, 10 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v index cd9cad4064..7bed956f3e 100644 --- a/test-suite/bugs/closed/HoTT_coq_123.v +++ b/test-suite/bugs/closed/HoTT_coq_123.v @@ -104,11 +104,15 @@ Record Functor (C D : PreCategory) := morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d) }. +(** Workaround to simpl losing universe constraints, see bug #5645. *) +Ltac simpl' := + simpl; match goal with [ |- ?P ] => let T := type of P in idtac end. + Global Instance trunc_forall `{Funext} `{P : A -> Type} `{forall a, IsTrunc n (P a)} : IsTrunc n (forall a, P a) | 100. Proof. generalize dependent P. - induction n as [ | n' IH]; (simpl; intros P ?). + induction n as [ | n' IH]; (simpl'; intros P ?). - admit. - pose (fun f g => trunc_equiv (@apD10 A P f g) ^-1); admit. Defined. diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index cfd489ddef..645320c603 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 |