diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 6 | ||||
| -rw-r--r-- | tactics/eauto.ml | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 8 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 10 |
6 files changed, 16 insertions, 16 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 4f7bb7ee1e..3287c1c354 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -99,7 +99,7 @@ let connect_hint_clenv h gl = let unify_resolve flags (h : hint) = Proofview.Goal.enter begin fun gl -> let clenv, c = connect_hint_clenv h gl in - Clenvtac.res_pf ~flags clenv + Clenv.res_pf ~flags clenv end let unify_resolve_nodelta h = unify_resolve auto_unif_flags h diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 56d6f7f09a..5ad21c2a5b 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -158,17 +158,17 @@ let e_give_exact flags h = in let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in Proofview.Unsafe.tclEVARS sigma <*> - Clenvtac.unify ~flags t1 <*> exact_no_check c + Clenv.unify ~flags t1 <*> exact_no_check c end let unify_e_resolve flags = begin fun gls (h, _) -> let clenv', c = connect_hint_clenv h gls in - Clenvtac.res_pf ~with_evars:true ~with_classes:false ~flags clenv' + Clenv.res_pf ~with_evars:true ~with_classes:false ~flags clenv' end let unify_resolve flags = begin fun gls (h, _) -> let clenv', _ = connect_hint_clenv h gls in - Clenvtac.res_pf ~with_evars:false ~with_classes:false ~flags clenv' + Clenv.res_pf ~with_evars:false ~with_classes:false ~flags clenv' end (** Application of a lemma using [refine] instead of the old [w_unify] *) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 7269228485..d275e15255 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -37,7 +37,7 @@ let e_give_exact ?(flags=eauto_unif_flags) c = if occur_existential sigma t1 || occur_existential sigma t2 then Tacticals.New.tclTHENLIST [Proofview.Unsafe.tclEVARS sigma; - Clenvtac.unify ~flags t1; + Clenv.unify ~flags t1; exact_no_check c] else exact_check c end @@ -68,7 +68,7 @@ open Auto let unify_e_resolve flags h = Proofview.Goal.enter begin fun gl -> let clenv', c = connect_hint_clenv h gl in - Clenvtac.res_pf ~with_evars:true ~with_classes:true ~flags clenv' + Clenv.res_pf ~with_evars:true ~with_classes:true ~flags clenv' end let hintmap_of sigma secvars concl = diff --git a/tactics/equality.ml b/tactics/equality.ml index 79b6dfe920..39017c946f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -154,7 +154,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let c1 = args.(arglen - 2) in let c2 = args.(arglen - 1) in let try_occ (evd', c') = - Clenvtac.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'} + Clenv.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'} in let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in let occs = @@ -1045,7 +1045,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf -> let pf_ty = mkArrow eqn Sorts.Relevant false_0 in let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in - let pf = Clenvtac.clenv_value_cast_meta absurd_clause in + let pf = Clenv.clenv_value_cast_meta absurd_clause in tclTHENS (assert_after Anonymous false_0) [onLastHypId gen_absurdity; (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))] @@ -1067,7 +1067,7 @@ let onEquality with_evars tac (c,lbindc) = let t = pf_get_type_of gl c in let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in - let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in + let eq_clause' = Clenv.clenv_pose_dependent_evars ~with_evars eq_clause in let eqn = clenv_type eq_clause' in (* FIXME evar leak *) let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in @@ -1397,7 +1397,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = let pf = applist(congr,[t;resty;injfun;t1;t2]) in let sigma, pf_typ = Typing.type_of env sigma pf in let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in - let pf = Clenvtac.clenv_value_cast_meta inj_clause in + let pf = Clenv.clenv_value_cast_meta inj_clause in let ty = simplify_args env sigma (clenv_type inj_clause) in evdref := sigma; Some (pf, ty) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 483d8a726b..22c5bbe73f 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -695,7 +695,7 @@ module New = struct in let branchtacs = List.init (Array.length branchsigns) after_tac in Proofview.tclTHEN - (Clenvtac.res_pf ~flags elimclause') + (Clenv.res_pf ~flags elimclause') (Proofview.tclEXTEND [] tclIDTAC branchtacs) end) end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index fd9fd81500..3133f9be1e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1373,7 +1373,7 @@ let do_replace id = function [id] is replaced by P using the proof given by [tac] *) let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac = - let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in + let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in let clenv = { clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd } @@ -1475,7 +1475,7 @@ let general_elim_clause with_evars flags where indclause elim = match where with | None -> let elimclause = clenv_fchain ~flags indmv elimclause indclause in - Clenvtac.res_pf elimclause ~with_evars ~with_classes:true ~flags + Clenv.res_pf elimclause ~with_evars ~with_classes:true ~flags | Some id -> let hypmv = match List.remove Int.equal indmv (clenv_independent elimclause) with @@ -1737,7 +1737,7 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars let n = nb_prod_modulo_zeta sigma thm_ty - nprod in if n<0 then error "Applied theorem does not have enough premises."; let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in - Clenvtac.res_pf clause ~with_evars ~flags + Clenv.res_pf clause ~with_evars ~flags with exn when noncritical exn -> let exn, info = Exninfo.capture exn in Proofview.tclZERO ~info exn @@ -4371,7 +4371,7 @@ let induction_tac with_evars params indvars elim = (* elimclause' is built from elimclause by instantiating all args and params. *) let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) - Clenvtac.res_pf ~with_evars ~flags:(elim_flags ()) elimclause' + Clenv.res_pf ~with_evars ~flags:(elim_flags ()) elimclause' end (* Apply induction "in place" taking into account dependent @@ -4812,7 +4812,7 @@ let elim_scheme_type elim t = (* t is inductive, then CUMUL or CONV is irrelevant *) clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t (clenv_meta_type clause mv) clause in - Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false + Clenv.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false | _ -> anomaly (Pp.str "elim_scheme_type.") end |