reparation bug moins unaire (erreur de PP)

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

7 files changed, 39 insertions, 15 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 26df4b837..338f4092a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -779,14 +779,15 @@ let make_current_scopes (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)
+    | "- _", [CNumeral(_,Bignat.POS p)] ->
+        CNotation (loc,ntn,[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,[CPatNotation(loc,"( _ )",l)])
     | _ -> CPatNotation (loc,ntn,l)
 
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b1ff0d623..19a705ec3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -395,6 +395,13 @@ let rec intern_cases_pattern scopes aliases tmp_scope = function
 	List.split (List.map2 (intern_cases_pattern scopes ([],[])) argscs pl)
       in
       (aliases::(List.flatten idsl), PatCstr (loc,c,pl',alias_of aliases))
+  | CPatNotation (loc,"- _",[CPatNumeral(_,Bignat.POS p)]) ->
+      let scopes = option_cons tmp_scope scopes in
+      ([aliases],
+      Symbols.interp_numeral_as_pattern loc (Bignat.NEG p)
+        (alias_of aliases) scopes)
+  | CPatNotation (_,"( _ )",[a]) ->
+      intern_cases_pattern scopes aliases tmp_scope a
   | CPatNotation (loc, ntn, args) ->
       let scopes = option_cons tmp_scope scopes in
       let (ids,c) = Symbols.interp_notation ntn scopes in
@@ -616,8 +623,8 @@ let internalise sigma env allow_soapp lvar c =
     | CNotation (loc,"- _",[CNumeral(_,Bignat.POS p)]) ->
         let scopes = option_cons tmp_scope scopes in
         Symbols.interp_numeral loc (Bignat.NEG p) scopes
+    | CNotation (_,"( _ )",[a]) -> intern env a
     | 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/interp/topconstr.ml b/interp/topconstr.ml
index 1ad9fd54c..23268556a 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -463,15 +463,18 @@ let mkProdC (idl,a,b)   = CProdN (dummy_loc,[idl,a],b)
 (* Used in correctness and interface *)
 
 
-let names_of_cases_indtype t =
-  let push_ref ids = function CRef (Ident (_,id)) -> id::ids | _ -> ids in
-  match t with
-  (* We deal only with the regular cases *)
-  | CApp (_,_,l) -> List.fold_left (fun ids (a,_) -> push_ref ids a) [] l
-  | CNotation (_,_,l)
-    (* assume the ntn is applicative and does not instantiate the head !! *)
-  | CAppExpl (_,_,l) -> List.fold_left push_ref [] l
-  | _ -> []
+let names_of_cases_indtype =
+  let rec vars_of ids t =
+    match t with
+      (* We deal only with the regular cases *)
+      | CApp (_,_,l) -> List.fold_left (fun ids (a,_) -> vars_of ids a) [] l
+      | CRef (Ident (_,id)) -> id::ids
+      | CNotation (_,_,l)
+      (* assume the ntn is applicative and does not instantiate the head !! *)
+      | CAppExpl (_,_,l) -> List.fold_left vars_of [] l
+      | CDelimiters(_,_,c) -> vars_of ids c
+      | _ -> ids in
+  vars_of []
 
 let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
 
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index e07e06b87..8aebc87bb 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -185,7 +185,8 @@ GEXTEND Gram
     | "0"
       [ c=atomic_constr -> c
       | c=match_constr -> c
-      | "("; c = operconstr LEVEL "250"; ")" -> c ] ]
+      | "("; c = operconstr LEVEL "250"; ")" ->
+          CNotation(loc,"( _ )",[c]) ] ]
   ;
   binder_constr:
     [ [ "forall"; bl = binder_list; ","; c = operconstr LEVEL "200" ->
@@ -303,8 +304,9 @@ GEXTEND Gram
     | "0"
       [ r = Prim.reference -> CPatAtom (loc,Some r)
       | "_" -> CPatAtom (loc,None)
-      | "("; p = pattern LEVEL "250"; ")" -> p
-      | n = bigint -> CPatNumeral (loc,n) ] ]
+      | "("; p = pattern LEVEL "250"; ")" ->
+          CPatNotation(loc,"( _ )",[p])
+      | n = INT -> CPatNumeral (loc,Bignat.POS(Bignat.of_string n)) ] ]
   ;
 (*
   lpattern:
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 22dd4d113..cdc7cc6f7 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -195,6 +195,8 @@ let rec pr_cases_pattern _inh = function
 	prlist_with_sep spc (pr_cases_pattern _inh) pl ++ str ")")
   | CPatAtom (_,Some c) -> pr_reference c
   | CPatAtom (_,None) -> str "_"
+  | CPatNotation (_,"( _ )",[p]) ->
+      str"("++ pr_cases_pattern _inh p ++ str")"
   | CPatNotation (_,s,env) -> fst (pr_notation pr_cases_pattern s env)
   | CPatNumeral (_,n) -> Bignat.pr_bigint n
   | CPatDelimiters (_,key,p) -> pr_delimiters key (pr_cases_pattern _inh p)
@@ -291,6 +293,8 @@ let rec pr inherited a =
   | CSort (_,s) -> pr_sort s, latom
   | CCast (_,a,b) ->
       hv 0 (pr (lcast,L) a ++ cut () ++ str "::" ++ pr (lcast,E) b), lcast
+  | CNotation (_,"( _ )",[t]) ->
+      str"("++ pr (max_int,E) t ++ str")", latom
   | CNotation (_,s,env) -> pr_notation pr s env
   | CNumeral (_,p) -> Bignat.pr_bigint p, latom
   | CDelimiters (_,sc,a) -> pr_delimiters sc (pr ltop a), latom
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 06b1b8bf9..57ca81de3 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -212,6 +212,9 @@ let rec mlexpr_of_constr = function
   | Topconstr.CCases (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.COrderedCase (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CHole loc -> <:expr< Topconstr.CHole $dloc$ >>
+  | Topconstr.CNotation(_,ntn,l) ->
+      <:expr< Topconstr.CNotation $dloc$ $mlexpr_of_string ntn$
+                $mlexpr_of_list mlexpr_of_constr l$ >>
   | Topconstr.CPatVar (loc,n) -> 
       <:expr< Topconstr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >>
   | _ -> failwith "mlexpr_of_constr: TODO"
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 2b37b945b..af8fb845d 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -131,6 +131,8 @@ let rec pr_patt inh p =
       prlist_with_sep sep (pr_patt (lapp,L)) args, lapp
   | CPatAtom (_,None) -> str "_", latom
   | CPatAtom (_,Some r) -> pr_reference r, latom
+  | CPatNotation (_,"( _ )",[p]) ->
+      str"("++ pr_patt (max_int,E) p ++ str")", latom
   | CPatNotation (_,s,env) -> pr_notation pr_patt s env
   | CPatNumeral (_,i) -> Bignat.pr_bigint i, latom
   | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt lsimple p), 1
@@ -512,6 +514,8 @@ let rec pr inherited a =
   | CSort (_,s) -> pr_sort s, latom
   | CCast (_,a,b) ->
       hv 0 (pr (lcast,L) a ++ cut () ++ str ":" ++ pr (-lcast,E) b), lcast
+  | CNotation (_,"( _ )",[t]) ->
+      str"("++ pr (max_int,L) t ++ str")", latom
   | CNotation (_,s,env) -> pr_notation pr s env
   | CNumeral (_,(Bignat.POS _ as p)) -> Bignat.pr_bigint p, lposint
   | CNumeral (_,(Bignat.NEG _ as p)) -> Bignat.pr_bigint p, lnegint