diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | Makefile.build | 6 | ||||
| -rw-r--r-- | Makefile.common | 6 | ||||
| -rw-r--r-- | man/coq-interface.1 | 4 | ||||
| -rw-r--r-- | man/coq-parser.1 (renamed from man/parser.1) | 4 | ||||
| -rwxr-xr-x | test-suite/check | 4 |
7 files changed, 15 insertions, 14 deletions
@@ -434,6 +434,7 @@ Tools - New stand-alone .vo files verifier "coqchk". - Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir". - New coqtop/coqc option -exclude-dir to exclude subdirs for option -R. +- The binary "parser" has been renamed to "coq-parser". Miscellaneous @@ -148,7 +148,7 @@ cruftclean: ml4clean indepclean: rm -f $(GENFILES) - rm -f $(COQTOPBYTE) $(COQCBYTE) bin/coq-interface$(EXE) bin/parser$(EXE) + rm -f $(COQTOPBYTE) $(COQCBYTE) bin/coq-interface$(EXE) bin/coq-parser$(EXE) find . -name '*~' -or -name '*.cm[ioa]' | xargs rm -f find contrib -name '*.vo' -or -name '*.glob' | xargs rm -f rm -f */*.pp[iox] contrib/*/*.pp[iox] @@ -177,7 +177,7 @@ docclean: archclean: clean-ide cleantheories rm -f $(COQTOPOPT) $(BESTCOQTOP) $(COQC) $(COQMKTOP) rm -f $(COQTOP) $(COQCOPT) $(COQMKTOPOPT) - rm -f bin/parser.opt$(EXE) bin/coq-interface.opt$(EXE) + rm -f bin/coq-parser.opt$(EXE) bin/coq-interface.opt$(EXE) find . -name '*.cmx' -or -name '*.cmxa' -or -name '*.[soa]' | xargs rm -f rm -f $(TOOLS) diff --git a/Makefile.build b/Makefile.build index 0475865c0..a0461d7a3 100644 --- a/Makefile.build +++ b/Makefile.build @@ -448,7 +448,7 @@ install-ide-info: $(INSTALLLIB) ide/FAQ $(FULLIDELIB) ########################################################################### -# Pcoq: special binaries for debugging (coq-interface, parser) +# Pcoq: special binaries for debugging (coq-interface, coq-parser) ########################################################################### # target to build Pcoq @@ -464,12 +464,12 @@ bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(INTERFACECMX) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ $(INTERFACECMX) -bin/parser$(EXE):$(LIBCOQRUN) $(PARSERCMO) +bin/coq-parser$(EXE):$(LIBCOQRUN) $(PARSERCMO) $(SHOW)'OCAMLC -o $@' $(HIDE)$(OCAMLC) -custom -linkall $(BYTEFLAGS) -o $@ \ dynlink.cma nums.cma $(LIBCOQRUN) $(CMA) $(PARSERCMO) -bin/parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX) +bin/coq-parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX) $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) -linkall $(OPTFLAGS) -o $@ \ $(LIBCOQRUN) nums.cmxa $(CMXA) $(PARSERCMX) diff --git a/Makefile.common b/Makefile.common index 3aacdef73..b068e72fb 100644 --- a/Makefile.common +++ b/Makefile.common @@ -377,9 +377,9 @@ PARSERREQUIRES:=$(LINKCMO) $(LIBCOQRUN) # Solution de facilité... PARSERREQUIRESCMX:=$(LINKCMX) ifeq ($(BEST),opt) - COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/parser$(EXE) bin/parser.opt$(EXE) + COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/coq-parser$(EXE) bin/coq-parser.opt$(EXE) else - COQINTERFACE:=bin/coq-interface$(EXE) bin/parser$(EXE) + COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-parser$(EXE) endif PARSERCODE:=contrib/interface/line_parser.cmo contrib/interface/vtp.cmo \ @@ -823,7 +823,7 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ man/coqwc.1 man/coqdoc.1 \ man/coq_makefile.1 man/coqmktop.1 -PCOQMANPAGES:=man/coq-interface.1 man/parser.1 +PCOQMANPAGES:=man/coq-interface.1 man/coq-parser.1 RECTYPESML:=kernel/term.ml library/nametab.ml proofs/tacexpr.ml \ parsing/pptactic.ml diff --git a/man/coq-interface.1 b/man/coq-interface.1 index 2ab2bf95f..ee013d952 100644 --- a/man/coq-interface.1 +++ b/man/coq-interface.1 @@ -1,7 +1,7 @@ .TH COQ 1 "April 25, 2001" .SH NAME -coq-interface \- +coq\-interface \- Customized Coq toplevel to make user interfaces .SH SYNOPSIS @@ -29,7 +29,7 @@ coq-interface (the same as coqtop). .BR coqc (1), .BR coqdep (1), .BR coqtop (1), -.BR parser (1). +.BR coq\-parser (1). .br .I The Coq Reference Manual. diff --git a/man/parser.1 b/man/coq-parser.1 index 051356b59..23dc82019 100644 --- a/man/parser.1 +++ b/man/coq-parser.1 @@ -1,11 +1,11 @@ .TH COQ 1 "April 25, 2001" .SH NAME -parser \- Coq parser +coq\-parser \- Coq parser .SH SYNOPSIS -.B parser +.B coq\-parser [ .B options ] diff --git a/test-suite/check b/test-suite/check index 571e7a67a..e4fd2a4c9 100755 --- a/test-suite/check +++ b/test-suite/check @@ -65,7 +65,7 @@ test_output() { done } -# La fonction suivante teste l'analyseur syntaxique fournit par "parser" +# La fonction suivante teste l'analyseur syntaxique fournit par "coq-parser" # Elle fonctionne comme test_output test_parser() { if [ -d $1 ]; then @@ -74,7 +74,7 @@ test_parser() { printf " "$f"..." tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` foutput=`dirname $f`/`basename $f .v`.out - echo "parse_file 1 \"$f\"" | ../bin/parser > $tmpoutput 2>&1 + echo "parse_file 1 \"$f\"" | ../bin/coq-parser > $tmpoutput 2>&1 perl -ne 'if(/Starting.*Parser Loop/){$printit = 1};print if $printit' \ $tmpoutput 2>&1 | grep -i error > /dev/null if [ $? = 0 ] ; then |