From 7f948efa4b8910037a053f7ab2a2f535b85e13c4 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Mon, 30 Sep 2013 16:09:50 +0000
Subject: lib/future: computations that are Exn can be replaced

A computation that is an exception morally holds no value
hence can be replaced by an type-equivalent computation.
This mechanism is used to edit broken proofs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16808 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/future.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'lib/future.ml')

diff --git a/lib/future.ml b/lib/future.ml
index 6001da30d7..c1fb176df6 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -47,6 +47,10 @@ let is_val x = match !x with
   | Val _ -> true
   | Exn _ | Closure _ | Delegated | Dropped -> false
 
+let is_exn x = match !x with
+  | Exn _ -> true
+  | Val _ | Closure _ | Delegated | Dropped -> false
+
 let peek_val x = match !x with
   | Val (v, _) -> Some v
   | Exn _ | Closure _ | Delegated | Dropped -> None
@@ -103,6 +107,11 @@ let chain ?(id="none") ?(pure=false) c f = ref (match !c with
 
 let create_here f = chain ~pure:false (from_here ()) f
 
+let replace x y =
+  match !x with
+  | Exn _ -> x := Closure (fun () -> force ~pure:false y)
+  | _ -> Errors.anomaly (Pp.str "Only Exn futures can be replaced")
+
 let purify f x =
   let state = !freeze () in
   try
-- 
cgit v1.2.3