From b103459011e65c09d481bdaee5fd7ce7638fb139 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 25 Sep 2008 20:16:23 +0000
Subject: Partial fix for bug #1948: recompute order of dependencies between
 evars at the end of unification as later evars can refer to previous ones.
 This removes the assumption that evars are already ordered in eterm's code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11419 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarutil.ml  | 23 ++++++++++++++++++++++-
 pretyping/evarutil.mli |  4 ++++
 2 files changed, 26 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 63a56f0d13..5491607153 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1054,7 +1054,28 @@ let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
   with e when precatchable_exception e ->
     (evd,false)
 
-
+let evars_of_term c = 
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (n, _) -> Intset.add n acc
+    | _ -> fold_constr evrec acc c
+  in 
+    evrec Intset.empty c
+
+let evars_of_named_context nc =
+  List.fold_right (fun (_, b, t) s ->
+    Option.fold_left (fun s t -> 
+      Intset.union s (evars_of_term t))
+      s b) nc Intset.empty
+
+let evars_of_evar_info evi =
+  Intset.union (evars_of_term evi.evar_concl)
+    (Intset.union 
+	(match evi.evar_body with 
+	| Evar_empty -> Intset.empty
+	| Evar_defined b -> evars_of_term b)
+	(evars_of_named_context (named_context_of_val evi.evar_hyps)))
+    
 (* [check_evars] fails if some unresolved evar remains *)
 (* it assumes that the defined existentials have already been substituted *)
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index d11e1fa2a5..ab9f8bebb1 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -94,6 +94,10 @@ val is_unification_pattern_evar : env -> existential -> constr list -> bool
 val is_unification_pattern : env -> constr -> constr array -> bool
 val solve_pattern_eqn : env -> constr list -> constr -> constr
 
+val evars_of_term : constr -> Intset.t
+val evars_of_named_context : named_context -> Intset.t
+val evars_of_evar_info : evar_info -> Intset.t
+
 (***********************************************************)
 (* Value/Type constraints *)
 
-- 
cgit v1.2.3