From a33f772631696c694f0d9a7fad3a914037c464b2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 26 Jun 2020 12:56:26 +0200 Subject: Refining out the Refiner. --- dev/base_include | 1 - proofs/proofs.mllib | 1 - proofs/refiner.ml | 9 --------- proofs/refiner.mli | 11 ----------- 4 files changed, 22 deletions(-) delete mode 100644 proofs/refiner.ml delete mode 100644 proofs/refiner.mli diff --git a/dev/base_include b/dev/base_include index 67ea3a1fa1..1f14fc2941 100644 --- 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 index 790a9dd2cc..5f19c1bb09 100644 --- 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 deleted file mode 100644 index b72d544151..0000000000 --- a/proofs/refiner.ml +++ /dev/null @@ -1,9 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(*