diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-03-02 13:08:59 +0100 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-03-02 13:09:30 +0100 |
commit | 022ec07048962ccd33ffdbcdc06adcb7fb09924f (patch) | |
tree | d8d1b3133a5f08e62072f5c001134cf7067def83 /pretyping/evarsolve.ml | |
parent | 7bad2a2caeeafdc05ec0d768b17bd6d7a7e3acd0 (diff) |
Fix bug #4097.
Diffstat (limited to 'pretyping/evarsolve.ml')
-rw-r--r-- | pretyping/evarsolve.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index f355d9a72..db7f6f677 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -179,23 +179,24 @@ let restrict_instance evd evk filter argsv = let noccur_evar env evd evk c = let cache = ref Int.Set.empty (* cache for let-ins *) in - let rec occur_rec k c = + let rec occur_rec (k, env as acc) c = match kind_of_term c with | Evar (evk',args' as ev') -> (match safe_evar_value evd ev' with - | Some c -> occur_rec k c + | Some c -> occur_rec acc c | None -> if Evar.equal evk evk' then raise Occur - else Array.iter (occur_rec k) args') + else Array.iter (occur_rec acc) args') | Rel i when i > k -> if not (Int.Set.mem (i-k) !cache) then (match pi2 (Environ.lookup_rel (i-k) env) with | None -> () - | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec k (lift i b)) - | Proj (p,c) -> occur_rec k (Retyping.expand_projection env evd p c []) - | _ -> iter_constr_with_binders succ occur_rec k c + | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b)) + | Proj (p,c) -> occur_rec acc (Retyping.expand_projection env evd p c []) + | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env)) + occur_rec acc c in - try occur_rec 0 c; true with Occur -> false + try occur_rec (0,env) c; true with Occur -> false (***************************************) (* Managing chains of local definitons *) |