aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tactics/class_tactics.ml18
-rw-r--r--tactics/eauto.ml6
-rw-r--r--tactics/eqdecide.ml3
-rw-r--r--tactics/equality.ml40
-rw-r--r--tactics/hipattern.ml47
-rw-r--r--tactics/hipattern.mli18
-rw-r--r--tactics/tactics.ml21
7 files changed, 75 insertions, 78 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 3fc2fc31b..36785b15d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1342,7 +1342,7 @@ module Search = struct
| Some i -> str ", with depth limit " ++ int i));
tac
- let run_on_evars p evm tac =
+ let run_on_evars p evm tac env =
match evars_to_goals p evm with
| None -> None (* This happens only because there's no evar having p *)
| Some (goals, evm') ->
@@ -1357,7 +1357,7 @@ module Search = struct
let pv = Proofview.unshelve goals pv in
try
let (), pv', (unsafe, shelved, gaveup), _ =
- Proofview.apply (Global.env ()) tac pv
+ Proofview.apply env tac pv
in
if Proofview.finished pv' then
let evm' = Proofview.return pv' in
@@ -1374,22 +1374,22 @@ module Search = struct
else raise Not_found
with Logic_monad.TacticFailure _ -> raise Not_found
- let evars_eauto depth only_classes unique dep st hints p evd =
+ let evars_eauto depth only_classes unique dep st hints p evd env =
let eauto_tac = eauto_tac ~st ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
- let res = run_on_evars p evd eauto_tac in
+ let res = run_on_evars p evd eauto_tac env in
match res with
| None -> evd
| Some evd' -> evd'
- let typeclasses_eauto ?depth unique st hints p evd =
- evars_eauto depth true unique false st hints p evd
+ let typeclasses_eauto ?depth unique st hints p evd env =
+ evars_eauto depth true unique false st hints p evd env
(** Typeclasses eauto is an eauto which tries to resolve only
goals of typeclass type, and assumes that the initially selected
evars in evd are independent of the rest of the evars *)
- let typeclasses_resolve debug depth unique p evd =
+ let typeclasses_resolve debug depth unique p evd env =
let db = searchtable_map typeclasses_db in
- typeclasses_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd
+ typeclasses_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd env
end
(** Binding to either V85 or Search implementations. *)
@@ -1534,7 +1534,7 @@ let resolve_all_evars debug depth unique env p oevd do_split fail =
if get_typeclasses_legacy_resolution () then
V85.resolve_all_evars_once debug depth unique p evd
else
- Search.typeclasses_resolve debug depth unique p evd
+ Search.typeclasses_resolve debug depth unique p evd env
in
if has_undefined p oevd evd' then raise Unresolved;
docomp evd' comps
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 64d4d3135..3d073c9dc 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -86,16 +86,16 @@ let rec prolog l n gl =
let prol = (prolog l (n-1)) in
(tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
-let out_term = function
+let out_term env = function
| IsConstr (c, _) -> c
- | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance (Global.env ()) gr))
+ | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr))
let prolog_tac l n =
Proofview.V82.tactic begin fun gl ->
let map c =
let (sigma, c) = c (pf_env gl) (project gl) in
let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in
- out_term c
+ out_term (pf_env gl) c
in
let l = List.map map l in
try (prolog l n gl)
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index d4cad3fa8..282b020ba 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -156,8 +156,9 @@ open Proofview.Notations
(* spiwack: a PatternMatchingFailure wrapper around [Hipattern]. *)
let match_eqdec sigma c =
+ Proofview.tclENV >>= fun env ->
try
- let (eqonleft,_,c1,c2,ty) = match_eqdec sigma c in
+ let (eqonleft,_,c1,c2,ty) = match_eqdec env sigma c in
let (op,eq1,noteq,eq2) =
match EConstr.kind sigma c with
| App (op,[|ty1;ty2|]) ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 66345ce43..d08735582 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -334,25 +334,27 @@ let (forward_general_setoid_rewrite_clause, general_setoid_rewrite_clause) = Hoo
(* Do we have a JMeq instance on twice the same domains ? *)
-let jmeq_same_dom gl = function
+let jmeq_same_dom env sigma = function
| None -> true (* already checked in Hipattern.find_eq_data_decompose *)
| Some t ->
- let rels, t = decompose_prod_assum (project gl) t in
- let env = push_rel_context rels (Proofview.Goal.env gl) in
- match decompose_app (project gl) t with
- | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2
+ let rels, t = decompose_prod_assum sigma t in
+ let env = push_rel_context rels env in
+ match decompose_app sigma t with
+ | _, [dom1; _; dom2;_] -> is_conv env sigma dom1 dom2
| _ -> false
(* find_elim determines which elimination principle is necessary to
eliminate lbeq on sort_of_gl. *)
-let find_elim hdcncl lft2rgt dep cls ot gl =
+let find_elim hdcncl lft2rgt dep cls ot =
+ Proofview.Goal.enter_one begin fun gl ->
let sigma = project gl in
let is_global gr c = Termops.is_global sigma gr c in
let inccl = Option.is_empty cls in
+ let env = Proofview.Goal.env gl in
if (is_global Coqlib.glob_eq hdcncl ||
(is_global Coqlib.glob_jmeq hdcncl &&
- jmeq_same_dom gl ot)) && not dep
+ jmeq_same_dom env sigma ot)) && not dep
then
let c =
match EConstr.kind sigma hdcncl with
@@ -382,9 +384,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
Logic.eq or Jmeq just before *)
assert false
in
- let (sigma, elim) = fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
- let elim = EConstr.of_constr elim in
- (sigma, (elim, Safe_typing.empty_private_constants))
+ pf_constr_of_global (ConstRef c)
else
let scheme_name = match dep, lft2rgt, inccl with
(* Non dependent case *)
@@ -400,14 +400,12 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
in
match EConstr.kind sigma hdcncl with
| Ind (ind,u) ->
+
let c, eff = find_scheme scheme_name ind in
- (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *)
- let (sigma, elim) =
- fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
- in
- let elim = EConstr.of_constr elim in
- (sigma, (elim, eff))
+ Proofview.tclEFFECTS eff <*>
+ pf_constr_of_global (ConstRef c)
| _ -> assert false
+ end
let type_of_clause cls gl = match cls with
| None -> Proofview.Goal.concl gl
@@ -420,9 +418,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d
let dep_fun = if isatomic then dependent else dependent_no_evar in
let type_of_cls = type_of_clause cls gl in
let dep = dep_proof_ok && dep_fun evd c type_of_cls in
- let (sigma, (elim, effs)) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
- Proofview.Unsafe.tclEVARS sigma <*>
- Proofview.tclEFFECTS effs <*>
+ find_elim hdcncl lft2rgt dep cls (Some t) >>= fun elim ->
general_elim_clause with_evars frzevars tac cls c t l
(match lft2rgt with None -> false | Some b -> b)
{elimindex = None; elimbody = (elim,NoBindings); elimrename = None}
@@ -536,7 +532,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
let do_hyps =
(* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
let ids gl =
- let ids_in_c = Termops.global_vars_set (Global.env()) (project gl) (fst c) in
+ let ids_in_c = Termops.global_vars_set (Proofview.Goal.env gl) (project gl) (fst c) in
let ids_of_hyps = pf_ids_of_hyps gl in
Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps
in
@@ -988,7 +984,7 @@ let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq =
let sigma, i = build_coq_I sigma in
let sigma, absurd_term = build_coq_False sigma in
let eq_elim, eff = ind_scheme_of_eq lbeq in
- let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in
+ let sigma, eq_elim = Evd.fresh_global env sigma eq_elim in
let eq_elim = EConstr.of_constr eq_elim in
sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term),
eff
@@ -1536,7 +1532,7 @@ let decomp_tuple_term env sigma c t =
let rec decomprec inner_code ex exty =
let iterated_decomp =
try
- let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose sigma ex in
+ let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose env sigma ex in
let car_code = applist (mkConstU (destConstRef p1,i),[a;p;inner_code])
and cdr_code = applist (mkConstU (destConstRef p2,i),[a;p;inner_code]) in
let cdrtyp = beta_applist sigma (p,[car]) in
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 4101004d4..b057cf72b 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -280,10 +280,7 @@ let coq_refl_jm_pattern =
open Globnames
-let is_matching sigma x y = is_matching (Global.env ()) sigma x y
-let matches sigma x y = matches (Global.env ()) sigma x y
-
-let match_with_equation sigma t =
+let match_with_equation env sigma t =
if not (isApp sigma t) then raise NoEquationFound;
let (hdapp,args) = destApp sigma t in
match EConstr.kind sigma hdapp with
@@ -302,11 +299,11 @@ let match_with_equation sigma t =
let constr_types = mip.mind_nf_lc in
let nconstr = Array.length mip.mind_consnames in
if Int.equal nconstr 1 then
- if is_matching sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then
+ if is_matching env sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then
None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
- else if is_matching sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then
+ else if is_matching env sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then
None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if is_matching sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then
+ else if is_matching env sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then
None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
else raise NoEquationFound
else raise NoEquationFound
@@ -335,8 +332,8 @@ let is_equality_type sigma t = op2bool (match_with_equality_type sigma t)
(** X1 -> X2 **)
let coq_arrow_pattern = mkPattern (mkGArrow (mkGPatVar "X1") (mkGPatVar "X2"))
-let match_arrow_pattern sigma t =
- let result = matches sigma coq_arrow_pattern t in
+let match_arrow_pattern env sigma t =
+ let result = matches env sigma coq_arrow_pattern t in
match Id.Map.bindings result with
| [(m1,arg);(m2,mind)] ->
assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind)
@@ -349,13 +346,13 @@ let match_with_imp_term sigma c =
let is_imp_term sigma c = op2bool (match_with_imp_term sigma c)
-let match_with_nottype sigma t =
+let match_with_nottype env sigma t =
try
- let (arg,mind) = match_arrow_pattern sigma t in
+ let (arg,mind) = match_arrow_pattern env sigma t in
if is_empty_type sigma mind then Some (mind,arg) else None
with PatternMatchingFailure -> None
-let is_nottype sigma t = op2bool (match_with_nottype sigma t)
+let is_nottype env sigma t = op2bool (match_with_nottype env sigma t)
(* Forall *)
@@ -481,7 +478,7 @@ let dest_nf_eq gls eqn =
(*** Sigma-types *)
-let match_sigma sigma ex =
+let match_sigma env sigma ex =
match EConstr.kind sigma ex with
| App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (Lazy.force coq_exist_ref) f ->
build_sigma (), (snd (destConstruct sigma f), a, p, car, cdr)
@@ -489,19 +486,19 @@ let match_sigma sigma ex =
build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr)
| _ -> raise PatternMatchingFailure
-let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
- match_sigma ex
+let find_sigma_data_decompose env ex = (* fails with PatternMatchingFailure *)
+ match_sigma env ex
(* Pattern "(sig ?1 ?2)" *)
let coq_sig_pattern =
lazy (mkPattern (mkGAppRef coq_sig_ref [mkGPatVar "X1"; mkGPatVar "X2"]))
-let match_sigma sigma t =
- match Id.Map.bindings (matches sigma (Lazy.force coq_sig_pattern) t) with
+let match_sigma env sigma t =
+ match Id.Map.bindings (matches env sigma (Lazy.force coq_sig_pattern) t) with
| [(_,a); (_,p)] -> (a,p)
| _ -> anomaly (Pp.str "Unexpected pattern.")
-let is_matching_sigma sigma t = is_matching sigma (Lazy.force coq_sig_pattern) t
+let is_matching_sigma env sigma t = is_matching env sigma (Lazy.force coq_sig_pattern) t
(*** Decidable equalities *)
@@ -533,15 +530,15 @@ let coq_eqdec_rev_pattern = coq_eqdec ~sum:coq_or_ref ~rev:true
let op_or = coq_or_ref
let op_sum = coq_sumbool_ref
-let match_eqdec sigma t =
+let match_eqdec env sigma t =
let eqonleft,op,subst =
- try true,op_sum,matches sigma (Lazy.force coq_eqdec_inf_pattern) t
+ try true,op_sum,matches env sigma (Lazy.force coq_eqdec_inf_pattern) t
with PatternMatchingFailure ->
- try false,op_sum,matches sigma (Lazy.force coq_eqdec_inf_rev_pattern) t
+ try false,op_sum,matches env sigma (Lazy.force coq_eqdec_inf_rev_pattern) t
with PatternMatchingFailure ->
- try true,op_or,matches sigma (Lazy.force coq_eqdec_pattern) t
+ try true,op_or,matches env sigma (Lazy.force coq_eqdec_pattern) t
with PatternMatchingFailure ->
- false,op_or,matches sigma (Lazy.force coq_eqdec_rev_pattern) t in
+ false,op_or,matches env sigma (Lazy.force coq_eqdec_rev_pattern) t in
match Id.Map.bindings subst with
| [(_,typ);(_,c1);(_,c2)] ->
eqonleft, Lazy.force op, c1, c2, typ
@@ -551,8 +548,8 @@ let match_eqdec sigma t =
let coq_not_pattern = lazy (mkPattern (mkGAppRef coq_not_ref [mkGHole]))
let coq_imp_False_pattern = lazy (mkPattern (mkGArrow mkGHole (mkGRef coq_False_ref)))
-let is_matching_not sigma t = is_matching sigma (Lazy.force coq_not_pattern) t
-let is_matching_imp_False sigma t = is_matching sigma (Lazy.force coq_imp_False_pattern) t
+let is_matching_not env sigma t = is_matching env sigma (Lazy.force coq_not_pattern) t
+let is_matching_imp_False env sigma t = is_matching env sigma (Lazy.force coq_imp_False_pattern) t
(* Remark: patterns that have references to the standard library must
be evaluated lazily (i.e. at the time they are used, not a the time
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 59406e158..8ff6fe95c 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -81,8 +81,8 @@ val is_inductive_equality : inductive -> bool
val match_with_equality_type : (constr * constr list) matching_function
val is_equality_type : testing_function
-val match_with_nottype : (constr * constr) matching_function
-val is_nottype : testing_function
+val match_with_nottype : Environ.env -> (constr * constr) matching_function
+val is_nottype : Environ.env -> testing_function
val match_with_forall_term : (Name.t * constr * constr) matching_function
val is_forall_term : testing_function
@@ -114,7 +114,7 @@ type equation_kind =
exception NoEquationFound
val match_with_equation:
- evar_map -> constr -> coq_eq_data option * constr * equation_kind
+ Environ.env -> evar_map -> constr -> coq_eq_data option * constr * equation_kind
(***** Destructing patterns bound to some theory *)
@@ -132,21 +132,21 @@ val find_eq_data : evar_map -> constr -> coq_eq_data * EInstance.t * equation_ki
(** Match a term of the form [(existT A P t p)]
Returns associated lemmas and [A,P,t,p] *)
-val find_sigma_data_decompose : evar_map -> constr ->
+val find_sigma_data_decompose : Environ.env -> evar_map -> constr ->
coq_sigma_data * (EInstance.t * constr * constr * constr * constr)
(** Match a term of the form [{x:A|P}], returns [A] and [P] *)
-val match_sigma : evar_map -> constr -> constr * constr
+val match_sigma : Environ.env -> evar_map -> constr -> constr * constr
-val is_matching_sigma : evar_map -> constr -> bool
+val is_matching_sigma : Environ.env -> evar_map -> constr -> bool
(** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns
[t,u,T] and a boolean telling if equality is on the left side *)
-val match_eqdec : evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr
+val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr
(** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr)
(** Match a negation *)
-val is_matching_not : evar_map -> constr -> bool
-val is_matching_imp_False : evar_map -> constr -> bool
+val is_matching_not : Environ.env -> evar_map -> constr -> bool
+val is_matching_imp_False : Environ.env -> evar_map -> constr -> bool
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cb905e749..5920b344d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3074,17 +3074,17 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
*)
-let warn_unused_intro_pattern =
+let warn_unused_intro_pattern env =
CWarnings.create ~name:"unused-intro-pattern" ~category:"tactics"
(fun names ->
strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern")
++ str": " ++ prlist_with_sep spc
(Miscprint.pr_intro_pattern
- (fun c -> Printer.pr_econstr (snd (c (Global.env()) Evd.empty)))) names)
+ (fun c -> Printer.pr_econstr (snd (c env Evd.empty)))) names)
-let check_unused_names names =
+let check_unused_names names env =
if not (List.is_empty names) then
- warn_unused_intro_pattern names
+ warn_unused_intro_pattern env names
let intropattern_of_name gl avoid = function
| Anonymous -> IntroNaming IntroAnonymous
@@ -3204,7 +3204,8 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names =
peel_tac ra' dests names thin)
end
| [] ->
- check_unused_names names;
+ Proofview.tclENV >>= fun env ->
+ check_unused_names names env;
Tacticals.New.tclTHEN (clear_wildcards thin) (tac dests)
in
peel_tac ra dests names []
@@ -3272,7 +3273,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
| Var id -> id
| _ ->
let type_of = Tacmach.New.pf_unsafe_type_of gl in
- id_of_name_using_hdchar (Global.env()) sigma (type_of c) Anonymous in
+ id_of_name_using_hdchar env sigma (type_of c) Anonymous in
let x = fresh_id_in_env avoid id env in
Tacticals.New.tclTHEN
(letin_tac None (Name x) c None allHypsAndConcl)
@@ -4485,7 +4486,7 @@ let induction_gen clear_flag isrec with_evars elim
declaring the induction argument as a new local variable *)
let id =
(* Type not the right one if partially applied but anyway for internal use*)
- let x = id_of_name_using_hdchar (Global.env()) evd t Anonymous in
+ let x = id_of_name_using_hdchar env evd t Anonymous in
new_fresh_id [] x gl in
let info_arg = (is_arg_pure_hyp, not enough_applied) in
pose_induction_arg_then
@@ -4521,8 +4522,9 @@ let induction_gen_l isrec with_evars elim names lc =
Proofview.Goal.enter begin fun gl ->
let type_of = Tacmach.New.pf_unsafe_type_of gl in
let sigma = Tacmach.New.project gl in
+ Proofview.tclENV >>= fun env ->
let x =
- id_of_name_using_hdchar (Global.env()) sigma (type_of c) Anonymous in
+ id_of_name_using_hdchar env sigma (type_of c) Anonymous in
let id = new_fresh_id [] x gl in
let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in
@@ -4741,8 +4743,9 @@ let prove_symmetry hdcncl eq_kind =
one_constructor 1 NoBindings ])
let match_with_equation sigma c =
+ Proofview.tclENV >>= fun env ->
try
- let res = match_with_equation sigma c in
+ let res = match_with_equation env sigma c in
Proofview.tclUNIT res
with NoEquationFound ->
Proofview.tclZERO NoEquationFound
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 09:21:55 +0000