aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--API/API.mli4
1 files changed, 1 insertions, 3 deletions
diff --git a/API/API.mli b/API/API.mli
index a90f8f84c..d1774afe5 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4389,9 +4389,7 @@ end
module Proof_type :
sig
- type prim_rule =
- | Cut of bool * bool * Names.Id.t * Term.types
- | Refine of Constr.t
+ type prim_rule = Refine of Constr.t
type tactic = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
end