aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/evar_refiner.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/evar_refiner.mli')
-rw-r--r--proofs/evar_refiner.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index b0dd5e4f4..55c7282c2 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -30,8 +30,6 @@ val rc_of_glsigma : goal sigma -> wc
dependent goal *)
type w_tactic = wc -> wc
-val local_Constraints : tactic
-
val startWalk : goal sigma -> wc * (wc -> tactic)
val extract_decl : evar -> w_tactic