diff options
| author | letouzey | 2011-02-11 13:28:47 +0000 |
|---|---|---|
| committer | letouzey | 2011-02-11 13:28:47 +0000 |
| commit | 8dd427c50a84aaba3a4187b214af913f5cff11ae (patch) | |
| tree | fb2154ee5baa8be195c4b5a1cc8c1708dfa8a0bb /pretyping | |
| parent | 7f828ca248861bf76aad26da7e418bf23aa22376 (diff) | |
In evars_of_term and co, visit array c in Evar(_,c) (sequel to r13809)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13833 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d1eb33cd6e..098d0d587a 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1365,10 +1365,10 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) let evars_of_term c = let rec evrec acc c = match kind_of_term c with - | Evar (n, _) -> Intset.add n acc + | Evar (n, l) -> Intset.add n (Array.fold_left evrec acc l) | _ -> fold_constr evrec acc c in - evrec Intset.empty c + evrec Intset.empty c let evars_of_named_context nc = List.fold_right (fun (_, b, t) s -> @@ -1393,7 +1393,8 @@ let evars_of_evar_info evi = let undefined_evars_of_term evd t = let rec evrec acc c = match kind_of_term c with - | Evar (n, _) -> (* TODO: should we look in the constr array ?? *) + | Evar (n, l) -> + let acc = Array.fold_left evrec acc l in (try match (Evd.find evd n).evar_body with | Evar_empty -> Intset.add n acc | Evar_defined c -> evrec acc c |