diff options
| author | msozeau | 2009-09-10 21:03:08 +0000 |
|---|---|---|
| committer | msozeau | 2009-09-10 21:03:08 +0000 |
| commit | d7609a04877b54dbf019cfd51abedacb955f1b20 (patch) | |
| tree | 86aa9c9cf2853ca80ab03d0c0af551bd0b8114d1 /plugins | |
| parent | e6ff6b0714a02a9d322360b66b4ae19423191345 (diff) | |
Misc fixes:
- better implicits for [antisymmetry]
- don't throw away implicit arguments info when doing [Program
Definition : type.]
- add standard debugging tactics to print goals/hyps in Program.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12317 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/subtac/subtac.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index ed8ecfac4f..8b1d20e6de 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -75,11 +75,13 @@ let start_proof_com env isevars sopt kind (bl,t) hook = next_global_ident_away false (id_of_string "Unnamed_thm") (Pfedit.get_all_proof_names ()) in - let evm, c, typ, _imps = + let evm, c, typ, imps = Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None in let c = solve_tccs_in_type env id isevars evm c typ in - Command.start_proof id kind c hook + Command.start_proof id kind c (fun loc gr -> + Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true imps; + hook loc gr) let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () |