From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- proofs/proofs.mllib | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'proofs/proofs.mllib') diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 32bf5576..804a5436 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -2,18 +2,13 @@ Miscprint Goal Evar_refiner Proof_using -Proof_type -Proof_errors -Logic_monad -Proofview_monad Logic -Proofview +Refine Proof Proof_global Redexpr Refiner Tacmach Pfedit -Tactic_debug Clenv Clenvtac -- cgit v1.2.3