Removing dead code, thanks to new OCaml warnings and a bit of scripting.

1 files changed, 0 insertions, 10 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index e74c4875fc..ab4f3af795 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -23,11 +23,6 @@ type clausenv = {
 				    out *)
   templtyp : constr freelisted (** its type *)}
 
-(** Substitution is not applied on templenv (because [subst_clenv] is
-   applied only on hints which typing env is overwritten by the
-   goal env) *)
-val subst_clenv : substitution -> clausenv -> clausenv
-
 (** subject of clenv (instantiated) *)
 val clenv_value     : clausenv -> constr
 
@@ -62,11 +57,6 @@ val clenv_unify :
 val clenv_unique_resolver :
   ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
 
-(** same as above ([allow_K=false]) but replaces remaining metas
-   with fresh evars if [evars_flag] is [true] *)
-val evar_clenv_unique_resolver :
-  ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
-
 val clenv_dependent : clausenv -> metavariable list
 
 val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv