aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic/JMeq.v
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-08 17:31:16 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-08 17:31:16 +0000
commit272194ae1dd0769105e1f485c9b96670a19008a7 (patch)
treed9a57bf8d1c4accc3b480f13279fea64ef333768 /theories/Logic/JMeq.v
parent0e3f27c1182c6a344a803e6c89779cfbca8f9855 (diff)
Restructuration of command.ml + generic infrastructure for inductive schemes
- Cleaning and uniformisation in command.ml: - For better modularity and better visibility, two files got isolated out of command.ml: - lemmas.ml is about starting and saving a proof - indschemes.ml is about declaring inductive schemes - Decomposition of the functions of command.ml into a functional part and the imperative part - Inductive schemes: - New architecture in ind_tables.ml for registering scheme builders, and for sharing and generating on demand inductive schemes - Adding new automatically generated equality schemes (file eqschemes.ml) - "_congr" for equality types (completing here commit 12273) - "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep", "_rew_backward" (similar to eq_rect), "_rew_backward_dep" for rewriting schemes (warning, rew_forward_dep cannot be stated following the standard Coq pattern for inductive types: "t=u" cannot be the last argument of the scheme) - "_case", "_case_nodep", "_case_dep" for case analysis schemes - Preliminary step towards discriminate and injection working on any equality-like type (e.g. eq_true) - Restating JMeq_congr under the canonical form of congruence schemes - Renamed "Set Equality Scheme" into "Set Equality Schemes" - Added "Set Rewriting Schemes", "Set Case Analysis Schemes" - Activation of the automatic generation of boolean equality lemmas - Partial debug and error messages improvements for the generation of boolean equality and decidable equality - Added schemes for making dependent rewrite working (unfortunately with not a fully satisfactory design - see file eqschemes.ml) - Some names of ML function made more regular (see dev/doc/changes.txt) - Incidentally, added a flush to obsolete Local/Global syntax warning git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/JMeq.v')
-rw-r--r--theories/Logic/JMeq.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 127be1134..83edf434e 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -80,9 +80,9 @@ intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
Qed.
Lemma JMeq_congr :
- forall (A B:Type) (f:A->B) (x y:A), JMeq x y -> JMeq (f x) (f y).
+ forall (A:Type) (x:A) (B:Type) (f:A->B) (y:A), JMeq x y -> f x = f y.
Proof.
-intros A B f x y H; case JMeq_eq with (1 := H); trivial.
+intros A x B f y H; case JMeq_eq with (1 := H); trivial.
Qed.
(** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *)