diff options
| -rw-r--r-- | tactics/equality.ml | 9 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 9 |
3 files changed, 9 insertions, 12 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index fcf954668..81f133ddc 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -34,7 +34,6 @@ open Coqlib open Declarations open Indrec open Clenv -open Clenvtac open Evd open Ind_tables open Eqschemes @@ -147,7 +146,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') = - clenv_pose_dependent_evars true {eqclause with evd = evd'} + Clenvtac.clenv_pose_dependent_evars true {eqclause with evd = evd'} in let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_unif_flags eqclause in let occs = @@ -892,7 +891,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort = discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in let pf_ty = mkArrow eqn absurd_term in let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in - let pf = clenv_value_cast_meta absurd_clause in + let pf = Clenvtac.clenv_value_cast_meta absurd_clause in Proofview.V82.tclEVARS sigma <*> Proofview.tclEFFECTS eff <*> tclTHENS (cut_intro absurd_term) @@ -918,7 +917,7 @@ let onEquality with_evars tac (c,lbindc) = let t = type_of 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' = clenv_pose_dependent_evars with_evars eq_clause in + let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in let eqn = clenv_type eq_clause' in let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in tclTHEN @@ -1263,7 +1262,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.e_type_of env sigma pf in let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in - let pf = clenv_value_cast_meta inj_clause in + let pf = Clenvtac.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 f647ac510..4d6893f1c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -16,7 +16,6 @@ open Context open Declarations open Tacmach open Clenv -open Clenvtac open Misctypes (************************************************************************) @@ -593,7 +592,7 @@ module New = struct in let branchtacs = List.init (Array.length branchsigns) after_tac in Proofview.tclTHEN - (Proofview.V82.tactic (clenv_refine false clenv')) + (Proofview.V82.tactic (Clenvtac.clenv_refine false clenv')) (Proofview.tclEXTEND [] tclIDTAC branchtacs) end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f65f295b2..1a3e84a1f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -28,7 +28,6 @@ open Genredexpr open Tacmach open Logic open Clenv -open Clenvtac open Refiner open Tacticals open Hipattern @@ -793,7 +792,7 @@ let check_unresolved_evars_of_metas clenv = [id] is replaced by P using the proof given by [tac] *) let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id clenv gl = - let clenv = clenv_pose_dependent_evars with_evars clenv in + let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv in let clenv = if with_classes then { clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd } @@ -844,7 +843,7 @@ let elimination_clause_scheme with_evars ?(flags=elim_flags ()) i (elim, elimty, (str "The type of elimination clause is not well-formed.")) in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in - res_pf elimclause' ~with_evars:with_evars ~flags gl + Clenvtac.res_pf elimclause' ~with_evars:with_evars ~flags gl (* * Elimination tactic with bindings and using an arbitrary @@ -3230,7 +3229,7 @@ let induction_tac_felim with_evars indvars nparams elim gl = let elimclause' = recolle_clenv nparams indvars elimclause gl in (* one last resolution (useless?) *) let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in - clenv_refine with_evars resolved gl + Clenvtac.clenv_refine with_evars resolved gl (* Apply induction "in place" replacing the hypothesis on which induction applies with the induction hypotheses *) @@ -3587,7 +3586,7 @@ let elim_scheme_type elim t gl = (* t is inductive, then CUMUL or CONV is irrelevant *) clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t (clenv_meta_type clause mv) clause in - res_pf clause' ~flags:(elim_flags ()) gl + Clenvtac.res_pf clause' ~flags:(elim_flags ()) gl | _ -> anomaly (Pp.str "elim_scheme_type") let elim_type t gl = |