diff options
| -rw-r--r-- | Makefile | 12 | ||||
| -rw-r--r-- | parsing/g_ltac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 11 |
3 files changed, 13 insertions, 12 deletions
@@ -207,8 +207,7 @@ INTERFACECMX=$(INTERFACE:.cmo=.cmx) ML4FILES += contrib/interface/debug_tac.ml4 contrib/interface/centaur.ml4 PARSERREQUIRES=$(CMO) # Solution de facilité... -PARSERREQUIRESCMX1=$(PARSERREQUIRES:.cmo=.cmx) -PARSERREQUIRESCMX=$(PARSERREQUIRESCMX1:.cma=.cmxa) +PARSERREQUIRESCMX=$(PARSERREQUIRES:.cmo=.cmx) ML4FILES += contrib/correctness/psyntax.ml4 contrib/omega/g_omega.ml4 \ contrib/romega/g_romega.ml4 contrib/ring/g_quote.ml4 \ @@ -298,7 +297,7 @@ CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) CMO=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) \ - $(PROOFS) $(TACTICS) $(INTERP) $(PARSING) $(TOPLEVEL) \ + $(INTERP) $(PARSING) $(PROOFS) $(TACTICS) $(TOPLEVEL) \ $(HIGHPARSING) $(HIGHTACTICS) $(CONTRIB) CMX=$(CMO:.cmo=.cmx) @@ -458,7 +457,7 @@ clean:: # tests ########################################################################### -check:: world +check:: world $(COQINTERFACE) cd test-suite; \ env COQBIN=../bin COQLIB=.. ./check -$(BEST) | tee check.log if grep -F 'Error!' test-suite/check.log ; then false; fi @@ -1229,13 +1228,14 @@ translation:: movenew:: -mv *.v8 theories/Init/ for i in theories/*/*.v8 contrib/*/*.v8; do \ - j=new`expr $$i : \\\\\(.*\\\\\)8` ; \ + if expr $$i : '.*/\*\.v8' > /dev/null ; then continue ; fi ; \ + j=new`dirname $$i`/`basename $$i .v8`.v ; \ mkdir -p `dirname $$j` ; \ mv -u -f $$i $$j ; \ done # 2. Build new syntax images and compile theories -newworld:: newinit newtheories newcontrib +newworld:: $(COQTOPNEW) newinit newtheories newcontrib newinit:: $(INITVO:%.vo=new%.vo) newtheories:: $(THEORIESVO:%.vo=new%.vo) diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 1cc0c0297..7519df465 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -225,7 +225,7 @@ GEXTEND Gram ; tactic_arg0: [ [ "("; a = tactic_expr; ")" -> arg_of_expr a - | "()" -> Integer 0 + | "()" -> TacVoid | r = reference -> Reference r | n = integer -> Integer n | id = METAIDENT -> MetaIdArg (loc,id) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index dadef23dd..d60a4db73 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -327,14 +327,15 @@ GEXTEND Gram IDENT "Section"; id = base_ident -> VernacBeginSection id | IDENT "Chapter"; id = base_ident -> VernacBeginSection id ] ] ; - module_vardecls: - [ [ "("; id = base_ident; idl = ident_comma_list_tail; - ":"; mty = Module.module_type; ")" - -> (id::idl,mty) ] ] + [ [ id = base_ident; idl = ident_comma_list_tail; ":"; + mty = Module.module_type -> (id::idl,mty) ] ] + ; + module_binders: + [ [ "["; bl = LIST1 module_vardecls SEP ";"; "]" -> bl ] ] ; module_binders_list: - [ [ bl = LIST0 module_vardecls -> bl ] ] + [ [ bls = LIST0 module_binders -> List.flatten bls ] ] ; of_module_type: [ [ ":"; mty = Module.module_type -> (mty, true) |