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 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_constrnew.ml4 | 8 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 4 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 3 |
3 files changed, 12 insertions, 3 deletions
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index e07e06b876..8aebc87bb4 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 22dd4d1135..cdc7cc6f76 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 06b1b8bf99..57ca81de38 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" |