From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 29 Sep 2006 12:46:59 +0000 (+0000)
Subject: ported to the new reflexivity implementation
X-Git-Tag: make_still_working~6835
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=afde27cb7aaaf833e20cca4f6a4a49571a8196a6;p=helm.git

ported to the new reflexivity implementation
---

diff --git a/helm/software/matita/matitaprover.ml b/helm/software/matita/matitaprover.ml
index d085b350c..5383493ed 100644
--- a/helm/software/matita/matitaprover.ml
+++ b/helm/software/matita/matitaprover.ml
@@ -41,6 +41,15 @@ theorem trans_eq :
 intros.elim H1.assumption.
 qed.
 
+default \"equality\"
+ " ^ buri ^ "/eq.ind
+ " ^ buri ^ "/sym_eq.con
+ " ^ buri ^ "/trans_eq.con
+ " ^ buri ^ "/eq_ind.con
+ " ^ buri ^ "/eq_elim_r.con
+ " ^ buri ^ "/eq_f.con
+ " ^ buri ^ "/eq_f1.con.
+
 theorem eq_f: \\forall  A,B:Type.\\forall f:A\\to B.
   \\forall x,y:A. eq A x y \\to eq B (f x) (f y).
 intros.elim H.reflexivity.
@@ -51,15 +60,6 @@ theorem eq_f1: \\forall  A,B:Type.\\forall f:A\\to B.
 intros.elim H.reflexivity.
 qed.
 
-default \"equality\"
- " ^ buri ^ "/eq.ind
- " ^ buri ^ "/sym_eq.con
- " ^ buri ^ "/trans_eq.con
- " ^ buri ^ "/eq_ind.con
- " ^ buri ^ "/eq_elim_r.con
- " ^ buri ^ "/eq_f.con
- " ^ buri ^ "/eq_f1.con.
-
 inductive ex (A:Type) (P:A \\to Prop) : Prop \\def
     ex_intro: \\forall x:A. P x \\to ex A P.
 interpretation \"exists\" 'exists \\eta.x =