diff options
Diffstat (limited to 'proofs/clenvtac.ml')
| -rw-r--r-- | proofs/clenvtac.ml | 47 |
1 files changed, 25 insertions, 22 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 769a9572..9bc818e8 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: clenvtac.ml 12102 2009-04-24 10:48:11Z herbelin $ *) +(* $Id$ *) open Pp open Util @@ -30,34 +30,34 @@ open Pattern open Tacexpr open Clenv - + (* This function put casts around metavariables whose type could not be * infered by the refiner, that is head of applications, predicates and * subject of Cases. * Does check that the casted type is closed. Anyway, the refiner would * fail in this case... *) -let clenv_cast_meta clenv = +let clenv_cast_meta clenv = let rec crec u = match kind_of_term u with | App _ | Case _ -> crec_hd u | Cast (c,_,_) when isMeta c -> u | _ -> map_constr crec u - + and crec_hd u = match kind_of_term (strip_outer_cast u) with - | Meta mv -> - (try + | Meta mv -> + (try let b = Typing.meta_type clenv.evd mv in - if occur_meta b then - raise (RefinerError (MetaInType b)); - mkCast (mkMeta mv, DEFAULTcast, b) + assert (not (occur_meta b)); + if occur_meta b then u + else mkCast (mkMeta mv, DEFAULTcast, b) with Not_found -> u) - | 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) - | _ -> u - in + | 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) + | _ -> u + in crec let clenv_value_cast_meta clenv = @@ -70,16 +70,17 @@ let clenv_pose_dependent_evars with_evars clenv = (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); clenv_pose_metas_as_evars clenv dep_mvs - let clenv_refine with_evars ?(with_classes=true) clenv gls = let clenv = clenv_pose_dependent_evars with_evars clenv in - let evd' = - if with_classes then - Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd + let evd' = + if with_classes then + Typeclasses.resolve_typeclasses ~fail:(not with_evars) + clenv.env clenv.evd else clenv.evd in + let clenv = { clenv with evd = evd' } in tclTHEN - (tclEVARS (evars_of evd')) + (tclEVARS evd') (refine (clenv_cast_meta clenv (clenv_value clenv))) gls @@ -104,17 +105,19 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft open Unification let fail_quick_unif_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; + modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = false; modulo_delta = empty_transparent_state; + resolve_evars = false; + use_evars_pattern_unification = false; } (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) -let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = +let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = let env = pf_env gls in let evd = create_goal_evar_defs (project gls) in let evd' = w_unify false env CONV ~flags m n evd in - tclIDTAC {it = gls.it; sigma = evars_of evd'} + tclIDTAC {it = gls.it; sigma = evd'} let unify ?(flags=fail_quick_unif_flags) m gls = let n = pf_concl gls in unifyTerms ~flags m n gls |