From 94a759be56074ac66c5c96b0cc7722b395c4cf40 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 4 Aug 2014 15:44:19 +0200
Subject: Cleaning of the new implementation of the tactic monad.

* Add comments in the code (mostly imported from Monad.v)
* Inline duplicated module
* Clean up some artifacts due to the extracted code.
* [NonLogical.new_ref] -> [NonLogical.ref] (I don't even remember why I chose this name originally)
* Remove the now superfluous [Proof_errors] module (which was used to define exceptions to be used in the extracted code).
* Remove Monad.v
---
 proofs/proof_errors.ml | 12 ------------
 1 file changed, 12 deletions(-)
 delete mode 100644 proofs/proof_errors.ml

(limited to 'proofs/proof_errors.ml')

diff --git a/proofs/proof_errors.ml b/proofs/proof_errors.ml
deleted file mode 100644
index e543b0c8fd..0000000000
--- a/proofs/proof_errors.ml
+++ /dev/null
@@ -1,12 +0,0 @@
-exception Exception of exn
-exception Timeout
-exception TacticFailure of exn
-
-let _ = Errors.register_handler begin function
-  | Timeout -> Errors.errorlabstrm "Some timeout function" (Pp.str"Timeout!")
-  | Exception e -> Errors.print e
-  | TacticFailure e -> Errors.print e
-  | _ -> Pervasives.raise Errors.Unhandled
-end
-
-
-- 
cgit v1.2.3