From 9aab7ae10aa1d535734f336c4bce16d908576d65 Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 13 Nov 2003 18:02:09 +0000
Subject: 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
---
 interp/constrextern.ml | 18 ++++++++++++++++--
 interp/constrintern.ml |  4 ++++
 2 files changed, 20 insertions(+), 2 deletions(-)

(limited to 'interp')

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
-- 
cgit v1.2.3