diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-03 20:37:57 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-03 20:37:57 +0000 |
| commit | 57cb2e40d0fb6e65a82fd1cda7930b7a6f743c8f (patch) | |
| tree | f02b15a29d58552edd2447982c65f8d0ef4f7098 /pretyping/evarutil.ml | |
| parent | dff6f3dbed334ad1179cc1abf8708365c2309106 (diff) | |
Fix obvious bug in evars_of_named_context.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12049 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 6c8d4e3de..3511db6e4 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1172,8 +1172,9 @@ 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 - + (Intset.union s (evars_of_term t)) b) + nc Intset.empty + let evars_of_evar_info evi = Intset.union (evars_of_term evi.evar_concl) (Intset.union |