diff options
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 2 | ||||
| -rw-r--r-- | test-suite/Makefile | 5 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 19 |
3 files changed, 21 insertions, 5 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 52b158871b..98e80c7652 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1082,7 +1082,7 @@ function make_coq { copq_coq_gtk copy_coq_license - # make clean seems to br broken for 8.5pl2 + # make clean seems to be broken for 8.5pl2 # 1.) find | xargs fails on cygwin, can be fixed by sed -i 's|\| xargs rm -f|-exec rm -fv \{\} \+|' Makefile # 2.) clean of test suites fails with "cannot run complexity tests (no bogomips found)" # make clean diff --git a/test-suite/Makefile b/test-suite/Makefile index 39ef05269f..afaa48463b 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -408,6 +408,11 @@ modules/%.vo: modules/%.v misc: $(patsubst %.sh,%.log,$(wildcard misc/*.sh)) +misc/universes.log: misc/universes/all_stdlib.v + +misc/universes/all_stdlib.v: + cd .. && $(MAKE) test-suite/$@ + $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) @echo "TEST $<" $(HIDE){ \ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index eaf685b184..cf0e8e759f 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -126,6 +126,16 @@ let rec interp_vernac sid (loc,com) = let f = Loadpath.locate_file fname in load_vernac verbosely sid f | v -> + + (* XXX: We need to run this before add as the classification is + highly dynamic and depends on the structure of the + document. Hopefully this is fixed when VtBack can be removed + and Undo etc... are just interpreted regularly. *) + let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with + | VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _ -> true + | _ -> false + in + let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in (* Main STM interaction *) @@ -139,11 +149,12 @@ let rec interp_vernac sid (loc,com) = if check_proof then Stm.finish (); (* We could use a more refined criteria that depends on the - vernac. For now we imitate the old approach. *) - let hide_goals = !Flags.batch_mode || is_query v || !Flags.quiet || - not (Proof_global.there_are_pending_proofs ()) in + vernac. For now we imitate the old approach and rely on the + classification. *) + let print_goals = not !Flags.batch_mode && not !Flags.quiet && + is_proof_step && Proof_global.there_are_pending_proofs () in - if not hide_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); + if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); nsid in try |