diff options
Diffstat (limited to 'proofs/clenvtac.ml')
| -rw-r--r-- | proofs/clenvtac.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 7a1a14bde..112402bca 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -29,6 +29,7 @@ let clenv_cast_meta clenv = match kind_of_term u with | App _ | Case _ -> crec_hd u | Cast (c,_,_) when isMeta c -> u + | Proj (p, c) -> mkProj (p, crec_hd c) | _ -> map_constr crec u and crec_hd u = @@ -43,6 +44,7 @@ let clenv_cast_meta clenv = | App(f,args) -> mkApp (crec_hd f, Array.map crec args) | Case(ci,p,c,br) -> mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) + | Proj (p, c) -> mkProj (p, crec_hd c) | _ -> u in crec @@ -68,15 +70,15 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls = in let clenv = { clenv with evd = evd' } in tclTHEN - (tclEVARS evd') - (refine (clenv_cast_meta clenv (clenv_value clenv))) + (tclEVARS (Evd.clear_metas evd')) + (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gls open Unification let dft = default_unify_flags -let res_pf clenv ?(with_evars=false) ?(flags=dft) gls = +let res_pf clenv ?(with_evars=false) ?(flags=dft ()) gls = clenv_refine with_evars (clenv_unique_resolver ~flags clenv gls) gls (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en |