From e52a9fa8835eddf70d0c8e454470fb12eebef7cd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 30 Oct 2003 14:29:39 +0000
Subject: Parsing du moins unaire au niveau de l'application qui n'a pas besoin
 d'etre associative a gauche; gestion du signe dans le parseur pas dans
 l'interpreteur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 66851e70e8..97790d3633 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -586,9 +586,6 @@ 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 scopes = option_cons tmp_scope scopes in
 	let (ids,c) = Symbols.interp_notation ntn scopes in
-- 
cgit v1.2.3