diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-30 17:53:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:20:30 +0100 |
| commit | 5143129baac805d3a49ac3ee9f3344c7a447634f (patch) | |
| tree | 60fd3fb22fc95474454a6a60f3a8715bf7d766d0 /proofs/clenvtac.ml | |
| parent | a42795cc1c2a8ed3efa9960af920ff7b16d928f0 (diff) | |
Termops API using EConstr.
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) |