aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/logic.ml1
-rw-r--r--proofs/pfedit.ml1
2 files changed, 0 insertions, 2 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2eed0c2e9e..b4d5689319 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -26,7 +26,6 @@ open Proof_type
open Typeops
open Type_errors
open Coqast
-open Declare
open Retyping
open Evarutil
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 69534b82b3..4f8d8b07f2 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -18,7 +18,6 @@ open Declarations
open Entries
open Environ
open Evd
-open Declare
open Typing
open Tacmach
open Proof_trees