diff options
author | 2008-09-25 20:16:23 +0000 | |
---|---|---|
committer | 2008-09-25 20:16:23 +0000 | |
commit | b103459011e65c09d481bdaee5fd7ce7638fb139 (patch) | |
tree | 7729ca2f988096f6fc50dde32d76534326051874 /pretyping/evarutil.ml | |
parent | f9cbb56333230d81338f1d223e2c08343a1095eb (diff) |
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
Diffstat (limited to 'pretyping/evarutil.ml')
-rw-r--r-- | pretyping/evarutil.ml | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 63a56f0d1..549160715 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 *) |