2 files changed, 0 insertions, 33 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 82f4314456..424b785bc1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -465,22 +465,6 @@ let bring_hyps clsl gl =
 
 (* Resolution with missing arguments *)
 
-let collect_com lbind = 
-  map_succeed (function (Com,c)->c | _ -> failwith "Com") lbind
-
-let make_clenv_binding_apply wc (c,t) lbind = 
-  let largs = collect_com lbind in
-  let lcomargs = List.length largs in
-  if lcomargs = List.length lbind then 
-    let clause = mk_clenv_from wc (c,t) in
-    clenv_constrain_missing_args largs clause
-  else if lcomargs = 0 then 
-    let clause = mk_clenv_rename_from wc (c,t) in
-    clenv_match_args lbind clause
-  else 
-    errorlabstrm "make_clenv_bindings"
-      [<'sTR "Cannot mix bindings and free associations">]
-
 let apply_with_bindings  (c,lbind) gl = 
   let (wc,kONT) = startWalk gl in
   let t = w_hnf_constr wc (w_type_of wc c) in 
@@ -955,19 +939,6 @@ let elimination_clause_scheme kONT wc elimclause indclause gl =
 (* cast added otherwise tactics Case (n1,n2) generates (?f x y) and 
  * refine fails *)
 
-let make_clenv_binding wc (c,t) lbind = 
-  let largs    = collect_com lbind in
-  let lcomargs = List.length largs in 
-  if lcomargs = List.length lbind then 
-    let clause = mk_clenv_from wc (c,t) in  
-    clenv_constrain_dep_args largs clause
-  else if lcomargs = 0 then 
-    let clause = mk_clenv_rename_from wc (c,t) in  
-    clenv_match_args lbind clause
-  else 
-    errorlabstrm "make_clenv_bindings"
-      [<'sTR "Cannot mix bindings and free associations">]
-
 let type_clenv_binding wc (c,t) lbind = 
   clenv_instance_template_type (make_clenv_binding wc (c,t) lbind)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0644bc972a..c81e1436f9 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -18,10 +18,6 @@ open Tacticals
 
 (*s General functions. *)
 
-val make_clenv_binding_apply : 
-  walking_constraints -> constr * constr -> constr substitution  -> 
-    walking_constraints clausenv
-
 val type_clenv_binding : walking_constraints ->
   constr * constr -> constr substitution  -> constr