diff options
author | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:58:31 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:58:31 +0200 |
commit | d06cea3ce4526736b5d32ba1780dbbc87c37c981 (patch) | |
tree | 2c2ea5a4633a41cfd4451e1eefb79c171312c881 /plugins/subtac/subtac.ml | |
parent | aae7cec8d7f5048215b7ed06a8e94cb032bfd21a (diff) | |
parent | 8f4d4c66134804bbf2d2fe65c893b68387272d31 (diff) |
Merge commit 'upstream/8.3+dfsg' into experimental/master
Diffstat (limited to 'plugins/subtac/subtac.ml')
-rw-r--r-- | plugins/subtac/subtac.ml | 4 |
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 ())) () |