diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-20 14:22:40 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-20 14:22:40 +0000 |
| commit | b78925e69d3e8b0ff2567bf0574e1bd55b33aa93 (patch) | |
| tree | ef12e124ffef426bae708c94d9c2e4709fd6272a /toplevel | |
| parent | 2285dae8af54043090ce5f8a59aa4162679714c6 (diff) | |
Fixing test-suite
- bug in r15614: hnf was identity
- fix Print Assumptions
- bug in r15624: Dump glob of Print About only for Glob
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15630 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7942a6da2..011818c15 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -420,7 +420,7 @@ let smart_global r = Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr; gr -let dump_global r = +let dump_global r = let gr = Smartlocate.smart_global r in Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr @@ -1372,9 +1372,9 @@ let vernac_print = function msg_notice (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s) | PrintVisibility s -> msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s) - | PrintAbout qid -> - dump_global qid; msg_notice (print_about qid) - | PrintImplicit qid -> + | PrintAbout qid -> + msg_notice (print_about qid) + | PrintImplicit qid -> dump_global qid; msg_notice (print_impargs qid) | PrintAssumptions (o,r) -> (* Prints all the axioms and section variables used by a term *) |