Refining out the Refiner.

coq · Jun 29, 2020 · a33f772 · a33f772
1 parent d28af58
commit a33f772
Show file tree

Hide file tree

Showing 4 changed files with 0 additions and 22 deletions.
diff --git a/dev/base_include b/dev/base_include
@@ -114,7 +114,6 @@ open Logic
 open Proof
 open Proof_using
 open Redexpr
-open Refiner
 open Tacmach
 
 open Hints

diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
@@ -6,6 +6,5 @@ Proof
 Logic
 Goal_select
 Proof_bullet
-Refiner
 Tacmach
 Clenv
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
diff --git a/proofs/refiner.mli b/proofs/refiner.mli