diff options
| author | barras | 2003-11-18 18:54:38 +0000 |
|---|---|---|
| committer | barras | 2003-11-18 18:54:38 +0000 |
| commit | b04df941937814d3701c9d0f573d962d85f088cc (patch) | |
| tree | ea67fac2c2aa73271ca47393e49d2ff0d1ee10cf /interp/constrintern.ml | |
| parent | 9a33fa8f17adab845424b711e8099e743cf140f8 (diff) | |
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
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 9 |
1 files changed, 8 insertions, 1 deletions
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 |