From 05bd0ab1dd85764874ca077005dcaff5414589a5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 26 Sep 2017 16:37:26 +0200
Subject: Moving setting of "cleared" evar flag directly in Evd.restrict.

In particular, this fixes #5757 which used restrict_evar to refine the
information on the source of an evar, and which should have set the
"cleared" flag.

Also renaming flag "restricted" since it is not only about "clear".

I guess this is what we want in general, but I did not survey all uses
of restrict_evar so, maybe, this should be refined further.
---
 engine/evarutil.mli | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'engine/evarutil.mli')

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 14173e774d..ee0fae3d46 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -204,10 +204,6 @@ type clear_dependency_error =
 
 exception ClearDependencyError of Id.t * clear_dependency_error
 
-(* spiwack: marks an evar that has been "defined" by clear.
-    used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*)
-val cleared : bool Store.field
-
 val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
   Id.Set.t -> named_context_val * types
 
-- 
cgit v1.2.3