diff options
| -rw-r--r-- | pretyping/cases.ml | 26 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1784.v | 20 | ||||
| -rw-r--r-- | test-suite/success/LetPat.v | 8 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 6 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 12 |
5 files changed, 38 insertions, 34 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index e1c5beeea2..7c0ed946f5 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1586,28 +1586,28 @@ let prepare_predicate_from_arsign_tycon loc env evdref tomatchs sign arsign c = * tycon to make the predicate if it is not closed. *) +let is_dependent_on_rel x t = + match kind_of_term x with + Rel n -> not (noccur_with_meta n n t) + | _ -> false + let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function (* No type annotation *) | None -> (match tycon with | Some (None, t) -> - if noccur_with_meta 0 max_int t then - let names,pred = - prepare_predicate_from_tycon loc false env evdref tomatchs sign t - in - Some (build_initial_predicate false names pred) - else + if List.exists (fun (x,_) -> is_dependent_on_rel x t) tomatchs + then let arsign = extract_arity_signature env tomatchs sign in let env' = List.fold_right push_rels arsign env in let names = List.rev (List.map (List.map pi1) arsign) in let pred = prepare_predicate_from_arsign_tycon loc env' evdref tomatchs sign arsign t in - if eq_constr pred t then - let names,pred = - prepare_predicate_from_tycon loc false env evdref tomatchs sign t - in - Some (build_initial_predicate false names pred) - else - Some (build_initial_predicate true names pred) + Some (build_initial_predicate true names pred) + else + let names,pred = + prepare_predicate_from_tycon loc false env evdref tomatchs sign t + in + Some (build_initial_predicate false names pred) | _ -> None) (* Some type annotation *) diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v index 6778831d85..12c92a8f7f 100644 --- a/test-suite/bugs/closed/shouldsucceed/1784.v +++ b/test-suite/bugs/closed/shouldsucceed/1784.v @@ -58,30 +58,30 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} := match x with | I x => match y with - | I y => if (Z_eq_dec x y) then left else right - | S ys => right + | I y => if (Z_eq_dec x y) then in_left else in_right + | S ys => in_right end | S xs => match y with - | I y => right + | I y => in_right | S ys => let fix list_in (xs ys:list sv) {struct xs} : {slist_in xs ys} + {~slist_in xs ys} := match xs with - | nil => left + | nil => in_left | x::xs => let fix elem_in (ys:list sv) : {sin x ys}+{~sin x ys} := match ys with - | nil => right - | y::ys => if lt_dec x y then left else if elem_in - ys then left else right + | nil => in_right + | y::ys => if lt_dec x y then in_left else if elem_in + ys then in_left else in_right end in if elem_in ys then - if list_in xs ys then left else right - else right + if list_in xs ys then in_left else in_right + else in_right end - in if list_in xs ys then left else right + in if list_in xs ys then in_left else in_right end end. diff --git a/test-suite/success/LetPat.v b/test-suite/success/LetPat.v index 72c7cc1553..545b8aeb86 100644 --- a/test-suite/success/LetPat.v +++ b/test-suite/success/LetPat.v @@ -48,8 +48,8 @@ Definition identity_functor (c : category) : functor c c := fun x => x. Definition functor_composition (a b c : category) : functor a b -> functor b c -> functor a c := - let ' (A :& homA :& CA) := a in - let ' (B :& homB :& CB) := b in - let ' (C :& homB :& CB) := c in + let 'A :& homA :& CA := a in + let 'B :& homB :& CB := b in + let 'C :& homB :& CB := c in fun f g => - fun x : A => g (f x). + fun x => g (f x). diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 4765bf0eea..c7e199b62b 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -20,6 +20,8 @@ Require Import Coq.Program.Tactics. Require Import Coq.Relations.Relation_Definitions. Require Export Coq.Classes.RelationClasses. +Open Local Scope relation_scope. + Set Implicit Arguments. Unset Strict Implicit. @@ -445,7 +447,7 @@ Proof. Qed. Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B), - inverse (R ==> R') <->rel (inverse R ==> inverse R'). + inverse (R ==> R') <R> (inverse R ==> inverse R'). Proof. intros. unfold flip, respectful. @@ -591,5 +593,5 @@ Program Instance {A : Type} => all_inverse_impl_morphism : Qed. Lemma inverse_pointwise_relation A (R : relation A) : - pointwise_relation (inverse R) <->rel inverse (pointwise_relation (A:=A) R). + pointwise_relation (inverse R) <R> inverse (pointwise_relation (A:=A) R). Proof. reflexivity. Qed. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 3d5c6a7ee4..cb32b846d7 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -219,24 +219,26 @@ Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid Definition relation_equivalence {A : Type} : relation (relation A) := fun (R R' : relation A) => forall x y, R x y <-> R' x y. -Infix "<->rel" := relation_equivalence (at level 70). +Infix "<R>" := relation_equivalence (at level 70) : relation_scope. Class subrelation {A:Type} (R R' : relation A) := is_subrelation : forall x y, R x y -> R' x y. Implicit Arguments subrelation [[A]]. -Infix "->rel" := subrelation (at level 70). +Infix "-R>" := subrelation (at level 70) : relation_scope. Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A := fun x y => R x y /\ R' x y. -Infix "//\\" := relation_conjunction (at level 55). +Infix "/R\" := relation_conjunction (at level 55) : relation_scope. Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A := fun x y => R x y \/ R' x y. -Infix "\\//" := relation_disjunction (at level 55). +Infix "\R/" := relation_disjunction (at level 55) : relation_scope. + +Open Local Scope relation_scope. (** Relation equivalence is an equivalence, and subrelation defines a partial order. *) @@ -258,7 +260,7 @@ Program Instance subrelation_preorder : on the carrier. *) Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder := - partial_order_equivalence : relation_equivalence eqA (R //\\ flip R). + partial_order_equivalence : relation_equivalence eqA (R /R\ flip R). (** The equivalence proof is sufficient for proving that [R] must be a morphism |