Merge remote-tracking branch 'upstream/trunk' into trunk

3 files changed, 28 insertions, 27 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 5e223a0b48..7b01c1b663 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -5,7 +5,7 @@
 ##    //   #                                                                 ##
 ###############################################################################
 ## GNUMakefile for Coq @COQ_VERSION@
-  
+
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
 # To implement recursion we save the name of the main Makefile
@@ -65,8 +65,8 @@ TIMECMD?=
 STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)"
 
 # Coq binaries
-COQC     ?= $(TIMER) "$(COQBIN)coqc"
-COQCHK   ?= $(TIMER) "$(COQBIN)coqchk"
+COQC     ?= "$(COQBIN)coqc"
+COQCHK   ?= "$(COQBIN)coqchk"
 COQDEP   ?= "$(COQBIN)coqdep"
 GALLINA  ?= "$(COQBIN)gallina"
 COQDOC   ?= "$(COQBIN)coqdoc"
@@ -80,7 +80,7 @@ CAMLOPTLINK ?= $(OCAMLFIND) opt       -rectypes -thread
 CAMLDEP     ?= $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
 
 # DESTDIR is prepended to all installation paths
-DESTDIR ?= 
+DESTDIR ?=
 
 # Debug builds, typically -g to OCaml, -debug to Coq.
 CAMLDEBUG ?=
@@ -96,7 +96,7 @@ COQDEBUG ?=
 #
 # post-all::
 # 	echo "All done!"
-# 
+#
 # in @LOCAL_FILE@
 #
 ###############################################################################
@@ -106,7 +106,7 @@ COQDEBUG ?=
 
 # Flags #######################################################################
 #
-# We define a bunch of variables combining the parameters 
+# We define a bunch of variables combining the parameters
 
 SHOW := $(if $(VERBOSE),@true "",@echo "")
 HIDE := $(if $(VERBOSE),,@)
@@ -127,7 +127,7 @@ DYNLIB:=.cmxs
 endif
 
 COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS)
-COQCHKFLAGS?=-silent -o $(COQLIBS) 
+COQCHKFLAGS?=-silent -o $(COQLIBS)
 COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML)
 
 # The version of Coq being run and the version of coq_makefile that
@@ -155,7 +155,7 @@ COQLIBINSTALL = $(COQLIB)user-contrib
 COQDOCINSTALL = $(DOCDIR)user-contrib
 COQTOPINSTALL = $(COQLIB)toploop
 
-# Retro compatibility (DESTDIR is standard on Unix, DESTROOT is not) 
+# Retro compatibility (DESTDIR is standard on Unix, DESTROOT is not)
 ifneq "$(DSTROOT)" ""
 DESTDIR := $(DSTROOT)
 endif
@@ -248,7 +248,7 @@ ALLDFILES = $(addsuffix .d,$(ALLSRCFILES))
 
 # Compilation targets #########################################################
 
-all: 
+all:
 	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
 	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all
 	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
@@ -281,17 +281,17 @@ quick: $(VOFILES:.vo=.vio)
 .PHONY: quick
 
 vio2vo:
-	$(COQC) $(COQDEBUG) $(COQFLAGS) \
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
 		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
 .PHONY: vio2vo
 
 checkproofs:
-	$(COQC) $(COQDEBUG) $(COQFLAGS) \
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
 		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
 .PHONY: checkproofs
 
 validate: $(VOFILES)
-	$(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=))
+	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=))
 .PHONY: validate
 
 only: $(TGTS)
@@ -427,10 +427,10 @@ clean::
 	$(HIDE)rm -f $(CMOFILES)
 	$(HIDE)rm -f $(CMIFILES)
 	$(HIDE)rm -f $(CMAFILES)
-	$(HIDE)rm -f $(CMOFILES:.cmo=.cmx) 
+	$(HIDE)rm -f $(CMOFILES:.cmo=.cmx)
 	$(HIDE)rm -f $(CMXAFILES)
-	$(HIDE)rm -f $(CMXSFILES) 
-	$(HIDE)rm -f $(CMOFILES:.cmo=.o) 
+	$(HIDE)rm -f $(CMXSFILES)
+	$(HIDE)rm -f $(CMOFILES:.cmo=.o)
 	$(HIDE)rm -f $(CMXAFILES:.cmxa=.a)
 	$(HIDE)rm -f $(ALLDFILES)
 	$(HIDE)rm -f $(ALLNATIVEFILES)
@@ -513,26 +513,26 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
 	$(SHOW)'CAMLOPT -pack -o $@'
 	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
 
-# This rule is for _CoqProject with no .mllib nor .mlpack 
+# This rule is for _CoqProject with no .mllib nor .mlpack
 $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx
 	$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
 	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $<
 
 $(VOFILES): %.vo: %.v
 	$(SHOW)COQC $<
-	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $<
 
 # FIXME ?merge with .vo / .vio ?
 $(GLOBFILES): %.glob: %.v
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $<
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $<
 
 $(VFILES:.v=.vio): %.vio: %.v
 	$(SHOW)COQC -quick $<
-	$(HIDE)$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
+	$(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
 
 $(BEAUTYFILES): %.v.beautified: %.v
 	$(SHOW)'BEAUTIFY $<'
-	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $<
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $<
 
 $(GFILES): %.g: %.v
 	$(SHOW)'GALLINA $<'
@@ -600,7 +600,7 @@ byte:
 
 opt:
 	$(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)"
-.PHONY:	opt 
+.PHONY:	opt
 
 # This is deprecated.  To extend this makefile use
 # extension points and @LOCAL_FILE@
@@ -655,4 +655,3 @@ debug:
 .PHONY: debug
 
 .DEFAULT_GOAL := all
-
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index c68c34bbbd..9224cdafe8 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -74,7 +74,9 @@ let dot = '.' ( space+ | eof)
 rule coq_action = parse
   | "Require" space+
       { require_modifiers None lexbuf }
-  | "Local"? "Declare" space+ "ML" space+ "Module" space+
+  | "Local" space+ "Declare" space+ "ML" space+ "Module" space+
+      { modules [] lexbuf }
+  | "Declare" space+ "ML" space+ "Module" space+
       { modules [] lexbuf }
   | "Load" space+
       { load_file lexbuf }
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 932097607b..4dad16fd8c 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -247,16 +247,16 @@ let eval_print l coq =
       let to_id, need_unfocus = get_id id in
       after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq)
   | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] ->
-      eval_call (query (phrase,tip_id())) coq
+      eval_call (query (0,(phrase,tip_id()))) coq
   | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] ->
       let to_id, _ = get_id id in
-      eval_call (query (phrase, to_id)) coq
+      eval_call (query (0,(phrase, to_id))) coq
   | [ Tok(_,"WAIT") ] ->
       let phrase = "Stm Wait." in
-      eval_call (query (phrase,tip_id())) coq
+      eval_call (query (0,(phrase,tip_id()))) coq
   | [ Tok(_,"JOIN") ] ->
       let phrase = "Stm JoinDocument." in
-      eval_call (query (phrase,tip_id())) coq
+      eval_call (query (0,(phrase,tip_id()))) coq
   | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] ->
       let to_id, _ = get_id id in
       if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip"