diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Classes/RelationClasses.v | 2 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 6 |
2 files changed, 5 insertions, 3 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index c1d7f34ce..7c7362cad 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -284,7 +284,7 @@ Definition predicate_implication {l : list Type} := (** Notations for pointwise equivalence and implication of predicates. *) Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope. -Infix "-∙>" := predicate_implication (at level 70) : predicate_scope. +Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope. Open Local Scope predicate_scope. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 11f710997..d299d9dda 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Program.Equality"); compile-command: "make -C ../.. TIME='time'" -*- *) +(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U"); compile-command: "make -C ../.. TIME='time'" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -498,12 +498,13 @@ Ltac equations := set_eos ; | _ => nonrec_equations end. +(* Equations NoConfusion_nat (P : Prop) (x y : nat) : Prop := NoConfusion_nat P 0 0 := P -> P ; NoConfusion_nat P 0 (S y) := P ; NoConfusion_nat P (S x) 0 := P ; NoConfusion_nat P (S x) (S y) := (x = y -> P) -> P. -Debug Off. + Solve Obligations using equations. Equations noConfusion_nat (P : Prop) (x y : nat) (H : x = y) : NoConfusion_nat P x y := @@ -569,3 +570,4 @@ noConfusion_list P A (cons a x) (cons a x) refl := λ p : a = a -> x = x -> P, p Instance list_noconf A : NoConfusionPackage (list A) := NoConfusion := λ P, Π x y, x = y -> NoConfusion_list P A x y ; noConfusion := λ P x y, noConfusion_list P A x y. +*)
\ No newline at end of file |