aboutsummaryrefslogtreecommitdiff
path: root/proofs/clenv.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/clenv.mli')
-rw-r--r--proofs/clenv.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 1adfdb885a..4279ab4768 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -63,9 +63,6 @@ val clenv_unify :
?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
(** unifies the concl of the goal with the type of the clenv *)
-val old_clenv_unique_resolver :
- ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
-
val clenv_unique_resolver :
?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv