diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-03 20:20:35 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-04 16:34:12 +0100 |
| commit | bcba6d1bc9f769da593a3b01a12846f3e7a26a25 (patch) | |
| tree | f09be5662a73315b38a21f49afc0dd8b8407cf4b /pretyping/evd.ml | |
| parent | d1321c8d686cc0e392c8ae26beb8abe762258900 (diff) | |
Experimentally applying eager evar substitution at the same time as
eager meta substition in w_unify, so as to preserve compatibility
after PMP's move of (setoid) rewrite clauses from metas to
evars (fbbe491cfa).
Hoping it is compatible for non-rewrite uses of the eager meta flag,
and that it is not too costly.
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index a3c9e3963..f495a81e6 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1454,11 +1454,14 @@ let retract_coercible_metas evd = let metas = Metamap.smartmapi map evd.metas in !mc, set_metas evd metas -let subst_defined_metas bl c = +let subst_defined_metas_evars (bl,el) c = let rec substrec c = match kind_of_term c with | Meta i -> let select (j,_,_) = Int.equal i j in substrec (pi2 (List.find select bl)) + | Evar (evk,args) -> + let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.equal Constr.equal args args' in + substrec (pi3 (List.find select el)) | _ -> map_constr substrec c in try Some (substrec c) with Not_found -> None |