aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenv.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/clenv.mli')
-rw-r--r--proofs/clenv.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 7ecc26ec9..59b166ea0 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -49,7 +49,6 @@ val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
(** {6 linking of clenvs } *)
-val connect_clenv : Goal.goal sigma -> clausenv -> clausenv
val clenv_fchain :
?with_univs:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv