summaryrefslogtreecommitdiff
path: root/plugins/subtac
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
commit3e96002677226c0cdaa8f355938a76cfb37a722a (patch)
tree3ca96e142fdb68e464d2f5f403f315282b94f922 /plugins/subtac
parentf18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff)
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'plugins/subtac')
-rw-r--r--plugins/subtac/subtac.ml4
-rw-r--r--plugins/subtac/subtac_classes.ml8
-rw-r--r--plugins/subtac/subtac_command.ml4
-rw-r--r--plugins/subtac/subtac_obligations.ml2
4 files changed, 9 insertions, 9 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 ())) ()
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index b2bf9912..4927adbe 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtac_classes.ml 13328 2010-07-26 11:05:30Z herbelin $ i*)
+(*i $Id: subtac_classes.ml 13516 2010-10-07 19:09:38Z msozeau $ i*)
open Pretyping
open Evd
@@ -123,7 +123,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
match props with
| Inr term ->
let c = interp_casted_constr_evars evars env' term cty in
- Inr (c, subst)
+ Inr c
| Inl props ->
let get_id =
function
@@ -162,7 +162,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
let term = Termops.it_mkLambda_or_LetIn app (ctx' @ ctx) in
term, termtype
- | Inr (def, subst) ->
+ | Inr def ->
let termtype = it_mkProd_or_LetIn cty ctx in
let term = Termops.it_mkLambda_or_LetIn def ctx in
term, termtype
@@ -174,7 +174,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
let hook vis gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
let inst = Typeclasses.new_instance k pri global (ConstRef cst) in
- Impargs.declare_manual_implicits false gr ~enriching:false imps;
+ Impargs.declare_manual_implicits false gr ~enriching:false [imps];
Typeclasses.add_instance inst
in
let evm = Subtac_utils.evars_of_term !evars Evd.empty term in
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index e7dd7ef1..a83611a4 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -333,7 +333,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
if Impargs.is_implicit_args () || impls <> [] then
- Impargs.declare_manual_implicits false gr impls
+ Impargs.declare_manual_implicits false gr [impls]
in
let typ = it_mkProd_or_LetIn top_arity binders in
hook, name, typ
@@ -341,7 +341,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let typ = it_mkProd_or_LetIn top_arity binders_rel in
let hook l gr =
if Impargs.is_implicit_args () || impls <> [] then
- Impargs.declare_manual_implicits false gr impls
+ Impargs.declare_manual_implicits false gr [impls]
in hook, recname, typ
in
let fullcoqc = Evarutil.nf_evar !isevars def in
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 1424618f..b76d0cb0 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -211,7 +211,7 @@ let declare_definition prg =
in
let gr = ConstRef c in
if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
- Impargs.declare_manual_implicits false gr prg.prg_implicits;
+ Impargs.declare_manual_implicits false gr [prg.prg_implicits];
print_message (Subtac_utils.definition_message prg.prg_name);
progmap_remove prg;
prg.prg_hook local gr;