From ead31bf3e2fe220d02dec59dce66471cc2c66fce Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 11 Aug 2003 10:25:04 +0000
Subject: 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
---
 parsing/g_constr.ml4 | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'parsing/g_constr.ml4')

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