summaryrefslogtreecommitdiff
path: root/plugins/subtac/subtac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac/subtac.ml')
-rw-r--r--plugins/subtac/subtac.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 885f7fb6..90b409ba 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac.ml 13344 2010-07-28 15:04:36Z msozeau $ *)
+(* $Id: subtac.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
open Global
open Pp
@@ -80,7 +80,7 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
in
let c = solve_tccs_in_type env id isevars evm c typ in
Lemmas.start_proof id kind c (fun loc gr ->
- Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true imps;
+ 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 ())) ()