In manual implicit arguments mode, do not enrich implicits

by the automatically infered arguments.


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

4 files changed, 11 insertions, 14 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index f63ae3ecb..4a8ce920f 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -230,8 +230,8 @@ let new_class id par ar sup props =
 	    (DefinitionEntry proj_entry, IsDefinition Definition) 
 	  in
 	  let cref = ConstRef cst in
-	    Impargs.declare_manual_implicits false cref (Impargs.is_implicit_args()) arity_imps;
-	    Impargs.declare_manual_implicits false (ConstRef proj_cst) (Impargs.is_implicit_args()) (List.hd fieldimpls);
+	    Impargs.declare_manual_implicits false cref arity_imps;
+	    Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
 	    set_rigid cst;
 	    cref, [proj_name, Some proj_cst]
       | _ ->
@@ -321,7 +321,7 @@ let fail_on_free_vars = function
 	
 let instance_hook k pri global imps ?hook cst = 
   let inst = Typeclasses.new_instance k pri global cst in
-    Impargs.maybe_declare_manual_implicits false (ConstRef cst) false imps;
+    Impargs.maybe_declare_manual_implicits false (ConstRef cst) ~enriching:false imps;
     Typeclasses.add_instance inst;
     (match hook with Some h -> h cst | None -> ())
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9ae3f8e82..c8acd8113 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -136,7 +136,7 @@ let red_constant_entry bl ce = function
 let declare_global_definition ident ce local imps =
   let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
   let gr = ConstRef kn in
-    maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
+    maybe_declare_manual_implicits false gr imps;
     if local = Local && Flags.is_verbose() then
       msg_warning (pr_id ident ++ str" is declared as a global definition");
     definition_message ident;
@@ -189,7 +189,7 @@ let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) =
         let kn =
           declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in
 	let gr = ConstRef kn in
-	  maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
+	  maybe_declare_manual_implicits false gr imps;
         assumption_message ident;
         if local=Local & Flags.is_verbose () then
           msg_warning (pr_id ident ++ str" is declared as a parameter" ++
@@ -625,12 +625,10 @@ let declare_mutual_with_eliminations isrecord mie impls =
   let (_,kn) = declare_mind isrecord mie in    
     list_iter_i (fun i (indimpls, constrimpls) -> 
       let ind = (kn,i) in
-	maybe_declare_manual_implicits false (IndRef ind)
-	  (is_implicit_args()) indimpls;
+	maybe_declare_manual_implicits false (IndRef ind) indimpls;
 	list_iter_i
 	  (fun j impls -> 
-	    maybe_declare_manual_implicits false (ConstructRef (ind, succ j))
-	      (is_implicit_args()) impls)
+	    maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls)
 	  constrimpls)
       impls;
     if_verbose ppnl (minductive_message names);
@@ -785,7 +783,7 @@ let declare_fix boxed kind f def t imps =
   } in
   let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
   let gr = ConstRef kn in
-    maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
+    maybe_declare_manual_implicits false gr imps;
     gr
       
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
@@ -1209,7 +1207,7 @@ let start_proof_com kind thms hook =
             list_map_i (save_remaining_recthms kind body opaq) 1 other_thms in
         let thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
-	  maybe_declare_manual_implicits false ref (is_implicit_args ()) imps;
+	  maybe_declare_manual_implicits false ref imps;
 	  hook strength ref) thms_data in
       start_proof id kind t ?init_tac:rec_tac hook
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ae97a8db4..8ac103fba 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -198,8 +198,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
                   raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
 	      let refi = ConstRef kn in
 	      let constr_fi = mkConst kn in
-	      Impargs.maybe_declare_manual_implicits 
-		false refi (Impargs.is_implicit_args()) impls;
+	      Impargs.maybe_declare_manual_implicits false refi impls;
 	      if coe then begin
 	        let cl = Class.class_of_global (IndRef indsp) in
 	        Class.try_add_new_coercion_with_source refi Global cl
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 399c18c92..8f2d3c1e3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -751,7 +751,7 @@ let vernac_syntactic_definition lid =
   
 let vernac_declare_implicits local r = function
   | Some imps ->
-      Impargs.declare_manual_implicits local (global_with_alias r) false
+      Impargs.declare_manual_implicits local (global_with_alias r) ~enriching:false
 	(List.map (fun (ex,b,f) -> ex, (b,f)) imps)
   | None -> 
       Impargs.declare_implicits local (global_with_alias r)