From a980d38681f7ab9bfd8a180f2252ce573e3ff211 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 29 Aug 2017 14:53:45 +0200
Subject: Post-merge API fix.

---
 API/API.mli | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index a90f8f84c7..d1774afe54 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
-- 
cgit v1.2.3