diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-11 18:28:41 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-11 18:28:41 +0000 |
commit | 5953161cd65194e341b2f8255501e7a15de498ac (patch) | |
tree | 6e3baa7b3ac9f85d82399dc4fb62f121b3f695ec /theories/Program | |
parent | cb18488b07fb6f9ba3e6e7ac854bbe68aa630e39 (diff) |
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
Diffstat (limited to 'theories/Program')
-rw-r--r-- | theories/Program/Equality.v | 6 |
1 files changed, 4 insertions, 2 deletions
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 |