diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 13 | ||||
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 8 |
2 files changed, 17 insertions, 4 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7cd5962d86..d3ed5e78b4 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -389,7 +389,11 @@ optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) .PHONY: optfiles # FIXME, see Ralf's bugreport -quick: $(VOFILES:.vo=.vio) +# quick is deprecated, now renamed vio +vio: $(VOFILES:.vo=.vio) +.PHONY: vio +quick: vio + $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") .PHONY: quick vio2vo: @@ -397,8 +401,9 @@ vio2vo: -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) .PHONY: vio2vo +# quick2vo is undocumented quick2vo: - $(HIDE)make -j $(J) quick + $(HIDE)make -j $(J) vio $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ @@ -677,8 +682,8 @@ $(GLOBFILES): %.glob: %.v $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(VFILES:.v=.vio): %.vio: %.v - $(SHOW)COQC -quick $< - $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + $(SHOW)COQC -vio $< + $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(VFILES:.v=.vos): %.vos: %.v $(SHOW)COQC -vos $< diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index a44ddf7467..13913cabc3 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -547,6 +547,9 @@ rule coq_bol = parse comment lexbuf end else skipped_comment lexbuf in if eol then coq_bol lexbuf else coq lexbuf } + | space* "#[" { + let eol = begin backtrack lexbuf; body_bol lexbuf end + in if eol then coq_bol lexbuf else coq lexbuf } | eof { () } | _ @@ -643,6 +646,11 @@ and coq = parse Output.ident s None; let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } + | "#[" + { ignore(lexeme lexbuf); + Output.char '#'; Output.char '['; + let eol = body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } | space+ { Output.char ' '; coq lexbuf } | eof { () } |