erreurs lexicales dans les patterns (manquait des espaces)

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

5 files changed, 7 insertions, 9 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 77f470b8bf..fdfc540d26 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -213,7 +213,7 @@ let translucent_abst env = function
 
 let abst_value env = function
   | DOPN(Abst sp, args) ->
-    contract_abstraction (lookup_abst sp env) args
+      contract_abstraction (lookup_abst sp env) args
   | _ -> invalid_arg "abst_value"
 
 let defined_constant env = function
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index dd328059f7..1cc5ceca55 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -48,10 +48,8 @@ GEXTEND Gram
           let id2 = Ast.coerce_to_var "lc2" lc2 in
             <:ast< (PRODLIST $c [$id1][$id2]($SLAM $idl $body)) >>
       | "("; lc1 = lconstr; ")" -> lc1
-(*
       | "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" ->
           <:ast< (XTRA"$SOAPP" $lc1 ($LIST $cl)) >>
-*)
       | IDENT "Fix"; id = ident; "{"; fbinders = fixbinders; "}" ->
           <:ast< (FIX $id ($LIST $fbinders)) >>
       | IDENT "CoFix"; id = ident; "{"; fbinders = cofixbinders; "}" ->
diff --git a/tactics/pattern.ml b/tactics/pattern.ml
index 78fa139741..23b6da6e46 100644
--- a/tactics/pattern.ml
+++ b/tactics/pattern.ml
@@ -321,7 +321,7 @@ let match_with_equation  t =
 let is_equation t = op2bool (match_with_equation  t)
 
 let match_with_nottype t =
-  let notpat = put_pat mmk "(?1->?2)" in 
+  let notpat = put_pat mmk "(?1 -> ?2)" in 
   try 
     (match dest_somatch t notpat with
        | [arg;mind] when is_empty_type mind -> Some (mind,arg)
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 76efe0958e..4fcfc0264e 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -52,8 +52,8 @@ let true_pattern = put_pat mmk "True"
 let and_pattern   = put_pat mmk "(and ? ?)"
 let or_pattern    = put_pat mmk "(or ? ?)"
 let eq_pattern    = put_pat mmk "(eq ? ? ?)"
-let pi_pattern    = put_pat mmk "(x:?)((?)@[x])"
-let imply_pattern = put_pat mmk "?1->?2"
+let pi_pattern    = put_pat mmk "(x : ?)((?)@[x])"
+let imply_pattern = put_pat mmk "?1 -> ?2"
 let iff_pattern   = put_pat mmk "(iff ? ?)"
 let not_pattern   = put_pat mmk "(not ?1)"
 let mkIMP a b     = soinstance imply_pattern [a;b]    
@@ -120,7 +120,7 @@ let dyck_imply_intro = (dImp None)
     --------------
     A->B,A,Gamma |- G  (A Atomique)
  *)
-let atomic_imply_bot_pattern = put_pat mmk "?1->?2"
+let atomic_imply_bot_pattern = put_pat mmk "?1 -> ?2"
 
 let atomic_imply_step cls gls =
   let mvb = somatch (clause_type cls gls) atomic_imply_bot_pattern in 
@@ -190,7 +190,7 @@ let back_thru_1 id =
 
 let exact_last_hyp = onLastHyp (fun h -> exact (VAR (out_some h)))
 
-let imply_imply_bot_pattern = put_pat mmk "(?1->?2)->?3"
+let imply_imply_bot_pattern = put_pat mmk "(?1 -> ?2) -> ?3"
 
 let imply_imply_step cls gls =
   let h0 = out_some cls in (* (C->D)->B *)
diff --git a/theories/Zarith/auxiliary.v b/theories/Zarith/auxiliary.v
index 647f027c0c..bee3e0a234 100644
--- a/theories/Zarith/auxiliary.v
+++ b/theories/Zarith/auxiliary.v
@@ -203,7 +203,7 @@ Theorem dec_ge:(x,y:nat)(decidable (ge x y)).
 Intros x y; Unfold ge; Apply dec_le.
 Save.
 
-Theorem not_not : (P:Prop)(decidable P) -> (~~P) -> P.
+Theorem not_not : (P:Prop)(decidable P) -> (~(~P)) -> P.
 Unfold decidable; Tauto. Save.
 
 Theorem not_or : (A,B:Prop) ~(A\/B) -> ~A /\ ~B.