diff options
| -rw-r--r-- | pretyping/evarconv.ml | 8 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4955.v | 98 |
2 files changed, 102 insertions, 4 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b7e0535da..73f251243 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -97,19 +97,19 @@ let position_problem l2r = function | CONV -> None | CUMUL -> Some l2r -let occur_rigidly ev evd t = +let occur_rigidly (evk,_ as ev) evd t = let rec aux t = match kind_of_term (whd_evar evd t) with | App (f, c) -> if aux f then Array.exists aux c else false | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true | Proj (p, c) -> not (aux c) - | Evar (ev',_) -> if Evar.equal ev ev' then raise Occur else false + | Evar (evk',_) -> if Evar.equal evk evk' then raise Occur else false | Cast (p, _, _) -> aux p | Lambda _ | LetIn _ -> false | Const _ -> false | Prod (_, b, t) -> ignore(aux b || aux t); true | Rel _ | Var _ -> false - | Case _ -> false + | Case (_,_,c,_) -> if eq_constr (mkEvar ev) c then raise Occur else false in try ignore(aux t); false with Occur -> true (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose @@ -478,7 +478,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [eta;(* Postpone the use of an heuristic *) (fun i -> - if not (occur_rigidly (fst ev) i tR) then + if not (occur_rigidly ev i tR) then let i,tF = if isRel tR || isVar tR then (* Optimization so as to generate candidates *) diff --git a/test-suite/bugs/closed/4955.v b/test-suite/bugs/closed/4955.v new file mode 100644 index 000000000..dce1f764c --- /dev/null +++ b/test-suite/bugs/closed/4955.v @@ -0,0 +1,98 @@ +(* An example involving a first-order unification triggering a cyclic constraint *) + +Module A. +Notation "{ x : A | P }" := (sigT (fun x:A => P)). +Notation "( x ; y )" := (existT _ x y) : fibration_scope. +Open Scope fibration_scope. +Notation "p @ q" := (eq_trans p q) (at level 20). +Notation "p ^" := (eq_sym p) (at level 3). +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) +: P y := + match p with eq_refl => u end. +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only +parsing). +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with eq_refl => eq_refl end. +Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y): p # (f +x) = f y + := match p with eq_refl => eq_refl end. +Axiom transport_compose + : forall {A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f +x)), + transport (fun x => P (f x)) p z = transport P (ap f p) z. +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope object_scope with object. +Record PreCategory := { object :> Type ; morphism : object -> object -> Type }. +Delimit Scope functor_scope with functor. +Record Functor (C D : PreCategory) := + { object_of :> C -> D; + morphism_of : forall s d, morphism C s d -> morphism D (object_of s) +(object_of d) }. +Arguments object_of {C%category D%category} f%functor c%object : rename, simpl +nomatch. +Arguments morphism_of [C%category] [D%category] f%functor [s%object d%object] +m%morphism : rename, simpl nomatch. +Section path_functor. + Variable C : PreCategory. + Variable D : PreCategory. + + Local Notation path_functor'_T F G + := { HO : object_of F = object_of G + | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) +(GO d)) + HO + (morphism_of F) + = morphism_of G } + (only parsing). + Definition path_functor'_sig_inv (F G : Functor C D) : F = G -> +path_functor'_T F G + := fun H' + => (ap object_of H'; + (transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H'). + +End path_functor. +End A. + +(* A variant of it with more axioms *) + +Module B. +Notation "{ x : A | P }" := (sigT (fun x:A => P)). +Notation "( x ; y )" := (existT _ x y). +Notation "p @ q" := (eq_trans p q) (at level 20). +Notation "p ^" := (eq_sym p) (at level 3). +Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y. +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only +parsing). +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with eq_refl => eq_refl end. +Axiom apD : forall {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y), p # (f +x) = f y. +Axiom transport_compose + : forall {A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f +x)), + transport (fun x => P (f x)) p z = transport P (ap f p) z. +Record PreCategory := { object :> Type ; morphism : object -> object -> Type }. +Record Functor (C D : PreCategory) := + { object_of :> C -> D; + morphism_of : forall s d, morphism C s d -> morphism D (object_of s) +(object_of d) }. +Arguments object_of {C D} f c : rename, simpl nomatch. +Arguments morphism_of [C] [D] f [s d] m : rename, simpl nomatch. +Section path_functor. + Variable C D : PreCategory. + Local Notation path_functor'_T F G + := { HO : object_of F = object_of G + | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) +(GO d)) + HO + (morphism_of F) + = morphism_of G }. + Definition path_functor'_sig_inv (F G : Functor C D) : F = G -> +path_functor'_T F G + := fun H' + => (ap object_of H'; + (transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H'). + +End path_functor. +End B. |