From 5953161cd65194e341b2f8255501e7a15de498ac Mon Sep 17 00:00:00 2001 From: msozeau Date: Thu, 11 Sep 2008 18:28:41 +0000 Subject: Add enough information to correctly globalize recursive calls in inductive and recursive definitions and references to previous fields in record and classes definitions. Fixes the corresponding typesetting issue in coqdoc output. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11397 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Program/Equality.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'theories/Program') diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 11f710997e..d299d9dda6 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 *) (* 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 -- cgit v1.2.3