aboutsummaryrefslogtreecommitdiff
path: root/API
diff options
context:
space:
mode:
Diffstat (limited to 'API')
-rw-r--r--API/API.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/API/API.mli b/API/API.mli
index 6227f17c65..9a671b43b3 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4964,8 +4964,6 @@ sig
val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool
- val pf_is_matching : Goal.goal Evd.sigma -> Pattern.constr_pattern -> EConstr.constr -> bool
-
val pf_hyps_types : Goal.goal Evd.sigma -> (Names.Id.t * EConstr.types) list
val pr_gls : Goal.goal Evd.sigma -> Pp.t