diff options
| -rw-r--r-- | pretyping/unification.ml | 13 | ||||
| -rw-r--r-- | test-suite/success/sprop_uip.v | 27 |
2 files changed, 39 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 207a03d80f..32dd805b30 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -687,6 +687,17 @@ let eta_constructor_app env sigma f l1 term = | _ -> assert false) | _ -> assert false +(* If the terms are irrelevant, check that they have the same type. *) +let careful_infer_conv ~pb ~ts env sigma m n = + if Retyping.relevance_of_term env sigma m == Sorts.Irrelevant && + Retyping.relevance_of_term env sigma n == Sorts.Irrelevant + then + let tm = Retyping.get_type_of env sigma m in + let tn = Retyping.get_type_of env sigma n in + Option.bind (infer_conv ~pb:CONV ~ts env sigma tm tn) + (fun sigma -> infer_conv ~pb ~ts env sigma m n) + else infer_conv ~pb ~ts env sigma m n + let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top env cv_pb flags m n = let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn : subst0) curm curn = let cM = Evarutil.whd_head_evar sigma curm @@ -1127,7 +1138,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e None else let ans = match flags.modulo_conv_on_closed_terms with - | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n + | Some convflags -> careful_infer_conv ~pb:cv_pb ~ts:convflags env sigma m n | _ -> constr_cmp cv_pb env sigma flags m n in match ans with | Some sigma -> ans diff --git a/test-suite/success/sprop_uip.v b/test-suite/success/sprop_uip.v index eae1b75689..c9377727db 100644 --- a/test-suite/success/sprop_uip.v +++ b/test-suite/success/sprop_uip.v @@ -121,6 +121,33 @@ Proof. simpl. Fail check. Abort. +Module HoTTStyle. + (* a small proof which tests destruct in a tricky case *) + + Definition ap {A B} (f:A -> B) {x y} (e : seq x y) : seq (f x) (f y). + Proof. destruct e. reflexivity. Defined. + + Section S. + Context + (A : Type) + (B : Type) + (f : A -> B) + (g : B -> A) + (section : forall a, seq (g (f a)) a) + (retraction : forall b, seq (f (g b)) b). + + Lemma bla (P : B -> Type) (a : A) (F : forall a, P (f a)) + : seq_rect _ (f (g (f a))) (fun a _ => P a) (F (g (f a))) (f a) (retraction (f a)) = F a. + Proof. + lazy. + change (retraction (f a)) with (ap f (section a)). + destruct (section a). + reflexivity. + Qed. + End S. + +End HoTTStyle. + (* check that extraction doesn't fall apart on matches with special reduction *) Require Extraction. |