diff options
| -rw-r--r-- | pretyping/pretyping.ml | 27 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 5 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 8 |
3 files changed, 24 insertions, 16 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c114a922c0..83594466eb 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -696,12 +696,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct | IsType -> (pretype_type empty_valcon env evdref lvar c).utj_val in let evd,_ = consider_remaining_unif_problems env !evdref in - evdref := evd; c' + evdref := evd; + nf_isevar !evdref c' let pretype_gen evdref env lvar kind c = let c = pretype_gen_aux evdref env lvar kind c in evdref := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !evdref; - nf_evar (evars_of !evdref) c + nf_isevar !evdref c (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage @@ -730,7 +731,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let ise_pretype_gen fail_evar sigma env lvar kind c = let evdref = ref (Evd.create_evar_defs sigma) in - let c = pretype_gen evdref env lvar kind c in + let c = pretype_gen_aux evdref env lvar kind c in let evd,_ = consider_remaining_unif_problems env !evdref in if fail_evar then let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in @@ -755,17 +756,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct let understand_tcc_evars evdref env kind c = pretype_gen evdref env ([],[]) kind c - + let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = let evd, t = - if resolve_classes then - ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c - else - let evdref = ref (Evd.create_evar_defs sigma) in - let c = pretype_gen_aux evdref env ([],[]) (OfType exptyp) c in - !evdref, nf_isevar !evdref c - in - Evd.evars_of evd, t + let evdref = ref (Evd.create_evar_defs sigma) in + let c = + if resolve_classes then + pretype_gen evdref env ([],[]) (OfType exptyp) c + else + pretype_gen_aux evdref env ([],[]) (OfType exptyp) c + in !evdref, c + in Evd.evars_of evd, t end - + module Default : S = Pretyping_F(Coercion.Default) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index f368ed3791..b1dc7c8961 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -77,8 +77,11 @@ let clenv_pose_dependent_evars with_evars clenv = let clenv_refine with_evars clenv gls = let clenv = clenv_expand_metas clenv in let clenv = clenv_pose_dependent_evars with_evars clenv in + let evd' = Typeclasses.resolve_typeclasses ~fail:(not with_evars) + clenv.env clenv.evd + in tclTHEN - (tclEVARS (evars_of clenv.evd)) + (tclEVARS (evars_of evd')) (refine (clenv_value_cast_meta clenv)) gls diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index aa5aaed3b7..063f387ac3 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1438,7 +1438,7 @@ let solve_remaining_evars env initial_sigma evd c = Pretype_errors.error_unsolvable_implicit loc env sigma evi src None) | _ -> map_constr proc_rec c in - proc_rec c + proc_rec (Evarutil.nf_isevar !evdref c) let interp_gen kind ist sigma env (c,ce) = let (ltacvars,unbndltacvars as vars) = constr_list ist env in @@ -1466,6 +1466,10 @@ let interp_open_constr ccl ist sigma env cc = let evd,c = interp_gen (OfType ccl) ist sigma env cc in (evars_of evd,c) +let interp_open_type ccl ist sigma env cc = + let evd,c = interp_gen IsType ist sigma env cc in + (evars_of evd,c) + let interp_constr = interp_econstr (OfType None) let interp_type = interp_econstr IsType @@ -2200,7 +2204,7 @@ and interp_atomic ist gl = function h_mutual_cofix b (interp_fresh_ident ist gl id) (List.map f l) | TacCut c -> h_cut (pf_interp_type ist gl c) | TacAssert (t,ipat,c) -> - let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in + let c = (if t=None then interp_constr else interp_type) ist (project gl) (pf_env gl) c in abstract_tactic (TacAssert (t,ipat,inj_open c)) (Tactics.forward (Option.map (interp_tactic ist) t) (interp_intro_pattern ist gl ipat) c) |