Imported Upstream version 8.3upstream/8.3

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;