Added multiple implicit arguments rules per name.

Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]".

This should a priori be used with care (it might be a bit disturbing
seeing the same constant used with apparently incompatible signatures).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 5 insertions, 5 deletions

diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 8a47dab7c0..4a244553ee 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -79,7 +79,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 1db9d407da..a663d3db33 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -171,7 +171,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 397bda9b02..eb3abfa5ae 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -332,7 +332,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
@@ -340,7 +340,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 22cc745f6d..d61ca2bc8b 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;