diff options
| author | herbelin | 2003-10-13 09:14:45 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-13 09:14:45 +0000 |
| commit | aa49b010e2a7ff849c1569662d70bc251c056dfa (patch) | |
| tree | bfff334e729dfceccafccfaf8e1c450d6581d74d | |
| parent | d58eb14b26a3a0774bc16e130a7bc87adadd262d (diff) | |
Petits bugs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4612 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 593d0f7a3b..b9150a30e3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -509,8 +509,8 @@ let vernac_require import _ qidl = warning ("Module "^(string_of_qualid qid)^ " is now built-in and shouldn't be required")) qidl else - if not !Options.v7 then List.iter test_renamed_module qidl; - raise e + (if not !Options.v7 then List.iter test_renamed_module qidl; + raise e) let vernac_import export refl = let import_one ref = @@ -977,9 +977,9 @@ let vernac_show = function | None -> pr_open_subgoals () | Some n -> pr_nth_open_subgoal n) | ShowGoalImplicitly None -> - msg (Constrextern.with_implicits pr_open_subgoals ()) + Constrextern.with_implicits msg (pr_open_subgoals ()) | ShowGoalImplicitly (Some n) -> - msg (Constrextern.with_implicits pr_nth_open_subgoal n) + Constrextern.with_implicits msg (pr_nth_open_subgoal n) | ShowProof -> show_proof () | ShowNode -> show_node () | ShowScript -> show_script () |