moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Local devient Let

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

12 files changed, 36 insertions, 25 deletions

diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 4281505e73..ddc52f8127 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -150,10 +150,7 @@ Infix 4 "+" Aplus V8only 50 (left associativity).
 Infix 4 "*" Amult V8only 40 (left associativity).
 Notation "0" := Azero.
 Notation "1" := Aone.
-Notation "- 0" := (Aopp Azero) (at level 0) V8only (at level 10).
-Notation "- 1" := (Aopp Aone) (at level 0) V8only (at level 10).
-Notation "- x" := (Aopp x) (at level 0) 
-  V8only (at level 10, x at level 0).
+Notation "- x" := (Aopp x) (at level 0) V8only.
 
 Record Ring_Theory : Prop :=
 { Th_plus_sym  : (n,m:A) n + m == m + n;
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index d31dd69951..d6c19410f2 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -35,10 +35,7 @@ Infix 4 "+" Aplus V8only 50 (left associativity).
 Infix 4 "*" Amult V8only 40 (left associativity).
 Notation "0" := Azero.
 Notation "1" := Aone.
-Notation "- 0" := (Aopp Azero) (at level 0) V8only (at level 10).
-Notation "- 1" := (Aopp Aone) (at level 0) V8only (at level 10).
-Notation "- x" := (Aopp x) (at level 0)
-  V8only (at level 10, x at level 0).
+Notation "- x" := (Aopp x) (at level 0) V8only.
 
 Variable plus_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a+a1 == a0+a2.
 Variable mult_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a*a1 == a0*a2.
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index 429d0ab8ac..f22ad35165 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -420,11 +420,11 @@ $$
 \nlsep \TERM{specialize}~\OPT{\NT{int}}~\NT{constr-with-bindings}
 \nlsep \TERM{lapply}~\tacconstr
 %%
-\nlsep \TERM{simple_induction}~\NT{quantified-hyp}
+\nlsep \TERM{simple}~\TERM{induction}~\NT{quantified-hyp}
 \nlsep \TERM{induction}~\NT{induction-arg}~\OPT{\NT{with-names}}
        ~\OPT{\NT{eliminator}}
 \nlsep \TERM{double}~\TERM{induction}~\NT{quantified-hyp}~\NT{quantified-hyp}
-\nlsep \TERM{simple_destruct}~\NT{quantified-hyp}
+\nlsep \TERM{simple}~\TERM{destruct}~\NT{quantified-hyp}
 \nlsep \TERM{destruct}~\NT{induction-arg}~\OPT{\NT{with-names}}
        ~\OPT{\NT{eliminator}}
 \nlsep \TERM{decompose}~\TERM{record}~\tacconstr
@@ -816,7 +816,7 @@ $$
    \TERM{Theorem} ~\mid~ \TERM{Lemma} ~\mid~ \TERM{Fact} ~\mid~ \TERM{Remark}
 \SEPDEF
 \DEFNT{def-token}
-   \TERM{Definition} ~\mid~ \TERM{Local} ~\mid~
+   \TERM{Definition} ~\mid~ \TERM{Let} ~\mid~
    \OPT{\TERM{Local}}~\TERM{SubClass}
 \SEPDEF
 \DEFNT{assum-token}
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 1fe371f855..cf62d81230 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -724,6 +724,20 @@ let same c d = try check_same_type c d; true with _ -> false
 let make_current_scopes (scopt,scopes) = 
   option_fold_right push_scope scopt scopes
 
+let make_notation loc ntn l =
+  match ntn,l with
+    (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
+    | "- _", [CNumeral(_,Bignat.POS p)] -> CNotation (loc,"- ( _ )",l)
+    | _ -> CNotation (loc,ntn,l)
+
+let make_pat_notation loc ntn l =
+  match ntn,l with
+    (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
+    | "- _", [CPatNumeral(_,Bignat.POS p)] ->
+        CPatNotation (loc,"- ( _ )",l)
+    | _ -> CPatNotation (loc,ntn,l)
+
+
 (*
 let rec cases_pattern_expr_of_constr_expr = function
   | CRef r -> CPatAtom (dummy_loc,Some r)
@@ -837,7 +851,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 		      extern_cases_pattern_in_scope 
 		        (scopt,List.fold_right push_scope scl scopes) vars c)
                       subst in
-		  insert_pat_delimiters (CPatNotation (loc,ntn,l)) key)
+		  insert_pat_delimiters (make_pat_notation loc ntn l) key)
           | SynDefRule kn ->
  	      CPatAtom (loc,Some (Qualid (loc, shortest_qualid_of_syndef kn)))
 	with
@@ -1154,7 +1168,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 		      extern (* assuming no overloading: *) true
 		        (scopt,List.fold_right push_scope scl scopes) vars c)
                       subst in
-	          insert_delimiters (CNotation (loc,ntn,l)) key)
+	          insert_delimiters (make_notation loc ntn l) key)
           | SynDefRule kn ->
               CRef (Qualid (loc, shortest_qualid_of_syndef kn)) in
  	if args = [] then e 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f27b7e4ca5..44a0d3b1f7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -613,7 +613,11 @@ let internalise sigma env allow_soapp lvar c =
     | CLetIn (loc,(_,na),c1,c2) ->
 	RLetIn (loc, na, intern (reset_tmp_scope env) c1,
           intern (push_name_env lvar env na) c2)
+    | CNotation (loc,"- _",[CNumeral(_,Bignat.POS p)]) ->
+        let scopes = option_cons tmp_scope scopes in
+        Symbols.interp_numeral loc (Bignat.NEG p) scopes
     | CNotation (loc,ntn,args) ->
+        let ntn = if ntn = "- ( _ )" then "- _" else ntn in
 	let scopes = option_cons tmp_scope scopes in
 	let (ids,c) = Symbols.interp_notation ntn scopes in
 	let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index cad065329a..7714ddba78 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -173,8 +173,7 @@ GEXTEND Gram
       | c1 = operconstr; "->"; c2 = operconstr LEVEL"200" -> CArrow(loc,c1,c2)]
     | "10"
       [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args)
-      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args)
-      | "-"; n=INT -> CNumeral (loc,Bignat.NEG (Bignat.of_string n)) ]
+      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) ]
     | "9" [ ]
     | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 77a5d919bf..96805e87b0 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -351,13 +351,13 @@ GEXTEND Gram
       | IDENT "lapply"; c = constr -> TacLApply c
 
       (* Derived basic tactics *)
-      | IDENT "simple_induction"; h = quantified_hypothesis ->
+      | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
           TacSimpleInduction h
       | IDENT "induction"; c = induction_arg; ids = with_names; 
 	  el = OPT eliminator -> TacNewInduction (c,el,ids)
       | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
-      | IDENT "simple_destruct"; h = quantified_hypothesis ->
+      | IDENT "simple"; IDENT"destruct"; h = quantified_hypothesis ->
           TacSimpleDestruct h
       | IDENT "destruct"; c = induction_arg; ids = with_names;
 	  el = OPT eliminator -> TacNewDestruct (c,el,ids)
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index a3c92311cf..c91d1079c5 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -140,7 +140,7 @@ GEXTEND Gram
   ;
   def_token:
     [ [ "Definition" -> (fun _ _ -> ()), (Global, Definition)
-      | IDENT "Local" -> (fun _ _ -> ()), (Local, Definition)
+      | IDENT "Let" -> (fun _ _ -> ()), (Local, Definition)
       | IDENT "SubClass"  -> Class.add_subclass_hook, (Global, Coercion)
       | IDENT "Local"; IDENT "SubClass"  ->
           Class.add_subclass_hook, (Local, Coercion) ] ] 
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index d7bfd970f8..a4bffd1580 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -54,8 +54,8 @@ Uninterpreted Notation "x * y" (at level 3, right associativity)
 Uninterpreted V8Notation "x / y" (at level 40, left associativity).
 Uninterpreted Notation "x + y" (at level 4, left associativity).
 Uninterpreted V8Notation "x - y" (at level 50, left associativity).
-Uninterpreted V8Notation "- x" (at level 10, x at level 0).
-Uninterpreted V8Notation "/ x" (at level 10, right associativity).
+Uninterpreted V8Notation "- x" (at level 35, right associative).
+Uninterpreted V8Notation "/ x" (at level 35, right associativity).
 
 Uninterpreted V8Notation "x ^ y" (at level 30, left associativity).
 
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index f708f12d1d..33d6ce7861 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -40,8 +40,8 @@ let lfix = 200
 let larrow = 90
 let lcast = 100
 let lapp = 10
-let lposint = 1    (* above the argument of notation "- x" *)
-let lnegint = lapp (* above application *)
+let lposint = 0
+let lnegint = 35 (* must be consistent with Notation "- x" *)
 let ltop = (200,E)
 let lproj = 1
 let lsimple = (1,E)
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 491076b0be..72d4a56082 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -492,13 +492,13 @@ and pr_atom1 env = function
 		    pr_clauses pr_ident cls))
   (* Derived basic tactics *)
   | TacSimpleInduction h ->
-      hov 1 (str "simple_induction" ++ pr_arg pr_quantified_hypothesis h)
+      hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h)
   | TacNewInduction (h,e,ids) ->
       hov 1 (str "induction" ++ spc () ++
              pr_induction_arg (pr_constr env) h ++ pr_with_names ids ++
              pr_opt (pr_eliminator env) e)
   | TacSimpleDestruct h ->
-      hov 1 (str "simple_destruct" ++ pr_arg pr_quantified_hypothesis h)
+      hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h)
   | TacNewDestruct (h,e,ids) ->
       hov 1 (str "destruct" ++ spc () ++
              pr_induction_arg (pr_constr env) h ++ pr_with_names ids ++
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 9162049688..9e6aa0fe05 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -581,7 +581,7 @@ let rec pr_vernac = function
       let pr_def_token = function
         | Local, Coercion -> str"Coercion Local"
         | Global, Coercion -> str"Coercion"
-        | Local, Definition -> str"Local"
+        | Local, Definition -> str"Let"
         | Global, Definition -> str"Definition"
         | Local, SubClass -> str"Local SubClass"
         | Global, SubClass -> str"SubClass"