diff options
| author | herbelin | 2003-08-11 10:25:04 +0000 |
|---|---|---|
| committer | herbelin | 2003-08-11 10:25:04 +0000 |
| commit | ead31bf3e2fe220d02dec59dce66471cc2c66fce (patch) | |
| tree | f2dc8aa43dda43200654e8e28a7556f7b84ae200 /parsing/g_constr.ml4 | |
| parent | aad98c46631f3acb3c71ff7a7f6ae9887627baa8 (diff) | |
Nouvelle mouture du traducteur v7->v8
Option -v8 à coqtop lance coqtopnew
Le terminateur reste "." en v8
Ajout construction primitive CLetTuple/RLetTuple
Introduction typage dans le traducteur pour traduire les Case/Cases/Match
Ajout mutables dans RCases or ROrderedCase pour permettre la traduction
Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts
+ Bugs ou améliorations diverses
Raffinement affichage projections de Record/Structure.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 43dc060a5a..5904906b01 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -127,12 +127,12 @@ GEXTEND Gram operconstr: [ "10" RIGHTA [ "!"; f = global; args = LIST0 (operconstr LEVEL "9") -> - CAppExpl (loc, (false,f), args) + CAppExpl (loc, (None,f), args) (* | "!"; f = global; "with"; b = binding_list -> <:ast< (APPLISTWITH $f $b) >> *) - | f = operconstr; args = LIST1 constr91 -> CApp (loc, (false,f), args) ] + | f = operconstr; args = LIST1 constr91 -> CApp (loc, (None,f), args) ] | "9" RIGHTA [ c1 = operconstr; "::"; c2 = operconstr LEVEL "9" -> CCast (loc, c1, c2) ] | "8" RIGHTA @@ -196,7 +196,7 @@ GEXTEND Gram | "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" -> (match lc1 with | CPatVar (loc2,(false,n)) -> - CApp (loc,(false,CPatVar (loc2, (true,n))), List.map (fun c -> c, None) cl) + CApp (loc,(None,CPatVar (loc2, (true,n))), List.map (fun c -> c, None) cl) | _ -> Util.error "Second-order pattern-matching expects a head metavariable") | IDENT "Fix"; id = identref; "{"; fbinders = fixbinders; "}" -> @@ -208,7 +208,7 @@ GEXTEND Gram | s = sort -> CSort (loc, s) | v = global -> CRef v | n = bigint -> CNumeral (loc,n) - | "!"; f = global -> CAppExpl (loc,(false,f),[]) + | "!"; f = global -> CAppExpl (loc,(None,f),[]) | "'"; test_ident_colon; key = IDENT; ":"; c = constr; "'" -> CDelimiters (loc,key,c) ] ] ; |