Modification pour passage p-automates

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1753 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 15 insertions, 7 deletions

diff --git a/CHANGES b/CHANGES
index 16be22cba9..3b1e5bd1eb 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,5 +1,6 @@
 Différences V7.0beta / V7.0
-
+- Portage de Correctness
+- Réécriture de Extraction
 - Ajout de déclarations locales aux Record (record à la Randy).
 - Correction de bugs
    - Identity Coercion
diff --git a/dev/base_include b/dev/base_include
index 67a0d48f1b..2515cabd39 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -36,6 +36,7 @@ Topdirs.dir_directory Coq_config.camlp4lib;;
 
 let parse_com   = Pcoq.parse_string Pcoq.Constr.constr;;
 let parse_tac = Pcoq.parse_string Pcoq.Tactic.tactic;;
+let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
 
 (* For compatibility reasons *)
 let parse_ast = parse_com;;
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3d8653da03..766e6e0e95 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -51,7 +51,7 @@ let evar_apprec env isevars stack c =
 (* Precondition: one of the terms of the pb is an uninstanciated evar,
  * possibly applied to arguments. *)
 
-let rec evar_conv_x env isevars pbty term1 term2 =
+let rec evar_conv_x env isevars pbty term1 term2 = 
   let term1 = whd_ise1 (evars_of isevars) term1 in
   let term2 = whd_ise1 (evars_of isevars) term2 in
 (*
@@ -219,16 +219,19 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	      & (List.length l1 = List.length l2)
 	      & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2)
 	    and f2 () =
-	      evar_eqappr_x env isevars pbty (subst1 b1 c'1,l1)
-		(subst1 b2 c'2,l2)
+              let appr1 = evar_apprec env isevars l1 (subst1 b1 c'1)
+              and appr2 = evar_apprec env isevars l2 (subst1 b2 c'2)
+	      in evar_eqappr_x env isevars pbty appr1 appr2
 	    in 
 	    ise_try isevars [f1; f2]
 
 	| IsLetIn (_,b1,_,c'1), _ ->(* On fait commuter les args avec le Let *)
-	    evar_eqappr_x env isevars pbty (subst1 b1 c'1,l1) appr2
+	     let appr1 = evar_apprec env isevars l1 (subst1 b1 c'1)
+             in evar_eqappr_x env isevars pbty appr1 appr2
 
 	| _, IsLetIn (_,b2,_,c'2) ->
-	    evar_eqappr_x env isevars pbty appr1 (subst1 b2 c'2,l2)
+	    let appr2 = evar_apprec env isevars l2 (subst1 b2 c'2)
+            in evar_eqappr_x env isevars pbty appr1 appr2
 
 	| IsProd (n,c1,c'1), IsProd (_,c2,c'2) when l1=[] & l2=[] -> 
             evar_conv_x env isevars CONV c1 c2
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 35a25a46f6..81805c9c49 100755
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -211,7 +211,10 @@ Definition prodT_curry : (A,B,C:Type)(A->B->C)->(prodT A B)->C :=
 
 Hints Immediate sym_idT sym_not_idT : core v62.
 
-
 Syntactic Definition AllT := allT | 1.
 Syntactic Definition ExT := exT | 1.
 Syntactic Definition ExT2 := exT2 | 1.
+
+Implicits fstT [1 2].
+Implicits sndT [1 2].
+Implicits pairT [1 2].