Backtrack sur le commit du 30.11.2001

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

2 files changed, 24 insertions, 30 deletions

diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index 9005b60896..c955c57eff 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -12,38 +12,28 @@ Require Rbase.
 
 Recursive Tactic Definition Isrealint trm:=
   Match trm With
-  | [R0] -> Idtac
-  | [R1] -> Idtac
-  | [(Rplus ?1 ?2)] -> (Isrealint ?1);(Isrealint ?2)
-  | [(Rminus ?1 ?2)] -> (Isrealint ?1);(Isrealint ?2)
-  | [(Rmult ?1 ?2)] -> (Isrealint ?1);(Isrealint ?2)
-  | [(Ropp ?1)] -> (Isrealint ?1)
+  | [``0``] -> Idtac
+  | [``1``] -> Idtac
+  | [``?1+?2``] -> (Isrealint ?1);(Isrealint ?2)
+  | [``?1-?2``] -> (Isrealint ?1);(Isrealint ?2)
+  | [``?1*?2``] -> (Isrealint ?1);(Isrealint ?2)
+  | [``-?1``] -> (Isrealint ?1)
   | _ -> Fail.
 
-
-Tactic Definition Sup0 :=
+Recursive Tactic Definition Sup0 :=
   Match Context With
-  | [ |- (Rgt R1 R0) ] -> Unfold Rgt;Apply Rlt_R0_R1
-  | [ |- (Rgt (Rplus R1 ?1) R0) ] ->
-    Apply (Rgt_trans (Rplus R1 ?1) ?1 R0);
-    [Pattern 1 (Rplus R1 ?1);Rewrite Rplus_sym;Unfold Rgt;
-     Apply Rlt_r_r_plus_R1
-    |Sup0].
+  | [ |- ``1>0`` ] -> Unfold Rgt;Apply Rlt_R0_R1
+  | [ |- ``1+?1>0`` ] ->
+    Apply (Rgt_trans ``1+?1`` ?1 ``0``);
+    [Pattern 1 ``1+?1``;Rewrite Rplus_sym;Unfold Rgt;
+     Apply Rlt_r_r_plus_R1|Sup0].
 
 Tactic Definition DiscrR :=
-  Match Context With
-  | [ |- ~R1==R0 ] -> Red;Intro;Apply R1_neq_R0;Assumption
-  | [ |- ~((Rplus R1 ?1)==R0) ] -> (Isrealint ?1);Apply Rgt_not_eq;Sup0
-  | [ |- ~(Ropp ?1)==R0 ] -> (Isrealint ?1);Apply Ropp_neq; DiscrR
-  | [ |- ~(?1==?1) ] -> ElimType False
-  | [ |- ~(Rminus R0 ?1)==R0 ] -> (Isrealint ?1);Rewrite Rminus_Ropp; DiscrR
-  | [ |- ~(?1==?2) ] -> ((Isrealint ?1);(Isrealint ?2);
-    Apply Rminus_not_eq; Ring (Rminus ?1 ?2); 
+  Try Match Context With
+  | [ |- ~(?1==?2) ] ->
+    Isrealint ?1;Isrealint ?2;
+    Apply Rminus_not_eq; Ring ``?1-?2``; 
       (Match Context With
-      | [ |- ~(Rplus (Ropp R1) ?)==R0 ] -> 
-        Repeat Rewrite <-Ropp_distr1; DiscrR
-      | [ |- ? ] -> DiscrR)
-     Orelse (Apply Rminus_not_eq_right; DiscrR)).
-  
-
-
+      | [ |- ``-1+?<>0`` ] -> 
+        Repeat Rewrite <- Ropp_distr1;Apply Ropp_neq
+      | _ -> Idtac);Apply Rgt_not_eq;Sup0.
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 9600cdce34..21a33391c2 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -50,7 +50,6 @@ with rexpr2 : constr :=
 
 with rexpr0 : constr :=
   expr_id [ constr:global($c) ] -> [ $c ]
-| expr_hole [ "?" ] -> [ ? ]
 | expr_com [ "[" constr:constr($c) "]" ] -> [ $c ]
 | expr_appl [ "(" rapplication($a) ")" ] -> [ $a ]
 | expr_num [ rnumber($s) ] -> [ $s ]
@@ -58,6 +57,11 @@ with rexpr0 : constr :=
 | expr_div [ rexpr0($p) "/" rexpr0($c) ] -> [ (Rdiv $p $c) ]
 | expr_opp [ "-" rexpr0($c) ] -> [ (Ropp $c) ] 
 | expr_inv [ "/" rexpr0($c) ] -> [ (Rinv $c) ]
+| expr_meta [ meta($m) ] -> [ $m ]
+
+with meta : ast :=
+| rimpl [ "?" ] -> [ (ISEVAR) ]
+| rmeta [ "?" prim:number($n) ] -> [ (META $n) ]
 
 with rapplication : constr :=
   apply [ rapplication($p) rexpr($c1) ] -> [ ($p $c1) ]