diff options
Diffstat (limited to 'proofs/clenvtac.ml')
-rw-r--r-- | proofs/clenvtac.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 98b5bc8b0..d8a20e08b 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -33,12 +33,12 @@ let clenv_cast_meta clenv = | _ -> map_constr crec u and crec_hd u = - match kind_of_term (strip_outer_cast u) with + match kind_of_term (strip_outer_cast clenv.evd (EConstr.of_constr u)) with | Meta mv -> (try let b = Typing.meta_type clenv.evd mv in - assert (not (occur_meta b)); - if occur_meta b then u + assert (not (occur_meta clenv.evd (EConstr.of_constr b))); + if occur_meta clenv.evd (EConstr.of_constr b) then u else mkCast (mkMeta mv, DEFAULTcast, b) with Not_found -> u) | App(f,args) -> mkApp (crec_hd f, Array.map crec args) |