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

3 files changed, 23 insertions, 12 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 26df4b837c..338f4092a2 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 b1ff0d6236..19a705ec30 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 1ad9fd54c4..23268556a8 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