aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tactics/equality.ml14
-rw-r--r--tactics/ind_tables.ml19
-rw-r--r--tactics/ind_tables.mli2
-rw-r--r--vernac/auto_ind_decl.ml14
4 files changed, 23 insertions, 26 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8f2336c0e0..f3073acb0a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -411,8 +411,7 @@ let find_elim hdcncl lft2rgt dep cls ot =
match EConstr.kind sigma hdcncl with
| Ind (ind,u) ->
- let c, eff = find_scheme scheme_name ind in
- Proofview.tclEFFECTS eff <*>
+ find_scheme scheme_name ind >>= fun c ->
pf_constr_of_global (GlobRef.ConstRef c)
| _ -> assert false
end
@@ -1001,14 +1000,13 @@ let ind_scheme_of_eq lbeq to_kind =
let from_kind = inductive_sort_family mip in
(* use ind rather than case by compatibility *)
let kind = Elimschemes.nondep_elim_scheme from_kind to_kind in
- let c, eff = find_scheme kind (destIndRef lbeq.eq) in
- GlobRef.ConstRef c, eff
+ find_scheme kind (destIndRef lbeq.eq) >>= fun c ->
+ Proofview.tclUNIT (GlobRef.ConstRef c)
let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind =
build_coq_I () >>= fun i ->
- let eq_elim, eff = ind_scheme_of_eq lbeq to_kind in
- Proofview.tclEFFECTS eff <*>
+ ind_scheme_of_eq lbeq to_kind >>= fun eq_elim ->
pf_constr_of_global eq_elim >>= fun eq_elim ->
Proofview.tclUNIT
(applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2]))
@@ -1352,10 +1350,10 @@ let inject_if_homogenous_dependent_pair ty =
check_required_library ["Coq";"Logic";"Eqdep_dec"];
let new_eq_args = [|pf_get_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
let inj2 = lib_ref "core.eqdep_dec.inj_pair2" in
- let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
+ find_scheme (!eq_dec_scheme_kind_name()) ind >>= fun c ->
(* cut with the good equality and prove the requested goal *)
tclTHENLIST
- [Proofview.tclEFFECTS eff;
+ [
intro;
onLastHyp (fun hyp ->
Tacticals.New.pf_constr_of_global Coqlib.(lib_ref "core.eq.type") >>= fun ceq ->
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index ae27cf1019..9164a4ff26 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -165,23 +165,26 @@ and declare_scheme_dependence mode eff = function
let _, eff' = define_mutual_scheme kind mode [] mind in
Evd.concat_side_effects eff' eff
-let find_scheme_on_env_too kind ind =
- let s = DeclareScheme.lookup_scheme kind ind in
- s, Evd.empty_side_effects
-
let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
- try find_scheme_on_env_too kind ind
- with Not_found ->
+ let open Proofview.Notations in
+ match lookup_scheme kind ind with
+ | Some s ->
+ (* FIXME: we need to perform this call to reset the environment, since the
+ imperative scheme table is desynchronized from the monadic interface. *)
+ Proofview.tclEFFECTS Evd.empty_side_effects <*>
+ Proofview.tclUNIT s
+ | None ->
match Hashtbl.find scheme_object_table kind with
| s,IndividualSchemeFunction (f, deps) ->
let deps = match deps with None -> [] | Some deps -> deps ind in
let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in
- define_individual_scheme_base kind s f mode None ind eff
+ let c, eff = define_individual_scheme_base kind s f mode None ind eff in
+ Proofview.tclEFFECTS eff <*> Proofview.tclUNIT c
| s,MutualSchemeFunction (f, deps) ->
let deps = match deps with None -> [] | Some deps -> deps mind in
let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in
let ca, eff = define_mutual_scheme_base kind s f mode [] mind eff in
- ca.(i), eff
+ Proofview.tclEFFECTS eff <*> Proofview.tclUNIT ca.(i)
let define_individual_scheme kind mode names ind =
ignore (define_individual_scheme kind mode names ind)
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index 9259a4a540..09fb051194 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -59,7 +59,7 @@ val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -
(int * Id.t) list -> MutInd.t -> unit
(** Main function to retrieve a scheme in the cache or to generate it *)
-val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Evd.side_effects
+val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t Proofview.tactic
(** Like [find_scheme] but does not generate a constant on the fly *)
val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t option
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 5fb12092d7..ebea5e146c 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -442,7 +442,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
let sigma = Tacmach.New.project gl in
let env = Tacmach.New.pf_env gl in
let u,v = destruct_ind env sigma type_of_pq in
- let c, eff = find_scheme ~mode lb_scheme_key (fst u) (*FIXME*) in
+ find_scheme ~mode lb_scheme_key (fst u) (*FIXME*) >>= fun c ->
let lb_type_of_p = mkConst c in
Proofview.tclEVARMAP >>= fun sigma ->
let lb_args = Array.append (Array.append
@@ -453,7 +453,6 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
then lb_type_of_p else mkApp (lb_type_of_p,lb_args)
in
Tacticals.New.tclTHENLIST [
- Proofview.tclEFFECTS eff;
Equality.replace p q ; apply app ; Auto.default_auto]
end
@@ -499,7 +498,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
in if eq_ind (fst u) ind
then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ]
else (
- let c, eff = find_scheme bl_scheme_key (fst u) (*FIXME*) in
+ find_scheme bl_scheme_key (fst u) (*FIXME*) >>= fun c ->
let bl_t1 = mkConst c in
let bl_args =
Array.append (Array.append
@@ -511,7 +510,6 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
then bl_t1 else mkApp (bl_t1,bl_args)
in
Tacticals.New.tclTHENLIST [
- Proofview.tclEFFECTS eff;
Equality.replace_by t1 t2
(Tacticals.New.tclTHEN (apply app) (Auto.default_auto)) ;
aux q1 q2 ]
@@ -928,7 +926,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
let eq = eq () and tt = tt ()
and ff = ff () and bb = bb () in
let list_id = list_id lnamesparrec in
- let (_, eff) = find_scheme beq_scheme_kind ind in
+ find_scheme beq_scheme_kind ind >>= fun _ ->
let eqI = eqI ind lnamesparrec in
let avoid = ref [] in
let eqtrue x = mkApp(eq,[|bb;x;tt|]) in
@@ -951,13 +949,11 @@ let compute_dec_tact ind lnamesparrec nparrec =
let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in
let arfresh = Array.of_list fresh_first_intros in
let xargs = Array.sub arfresh 0 (2*nparrec) in
- let c, eff' = find_scheme bl_scheme_kind ind in
+ find_scheme bl_scheme_kind ind >>= fun c ->
let blI = mkConst c in
- let c, eff'' = find_scheme lb_scheme_kind ind in
+ find_scheme lb_scheme_kind ind >>= fun c ->
let lbI = mkConst c in
- let eff = (Evd.concat_side_effects eff'' (Evd.concat_side_effects eff' eff)) in
Tacticals.New.tclTHENLIST [
- Proofview.tclEFFECTS eff;
intros_using fresh_first_intros;
intros_using [freshn;freshm];
(*we do this so we don't have to prove the same goal twice *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:51:10 +0000