aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml7
-rw-r--r--proofs/proofview.ml9
-rw-r--r--proofs/proofview.mli4
-rw-r--r--tactics/extratactics.ml47
-rw-r--r--tactics/inv.ml3
-rw-r--r--tactics/rewrite.ml17
-rw-r--r--tactics/tactics.ml86
-rw-r--r--tactics/tactics.mli2
-rw-r--r--toplevel/classes.ml3
9 files changed, 89 insertions, 49 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index d8c5b8a95..1741df533 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -29,6 +29,7 @@ open Termops
open Namegen
open Goptions
open Misctypes
+open Sigma.Notations
(* Strictness option *)
@@ -1305,7 +1306,11 @@ let understand_my_constr env sigma c concl =
Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc)
let my_refine c gls =
- let oc sigma = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
+ let oc = { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
+ let (sigma, c) = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
+ Sigma.Unsafe.of_pair (c, sigma)
+ end } in
Proofview.V82.of_tactic (Tactics.New.refine oc) gls
(* end focus/claim *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 11b7d07d0..f549913f2 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -16,6 +16,7 @@
open Pp
open Util
open Proofview_monad
+open Sigma.Notations
(** Main state of tactics *)
type proofview = Proofview_monad.proofview
@@ -1031,7 +1032,7 @@ struct
let prev_future_goals = Evd.future_goals sigma in
let prev_principal_goal = Evd.principal_future_goal sigma in
(** Create the refinement term *)
- let (sigma, c) = f (Evd.reset_future_goals sigma) in
+ let (c, sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
let evs = Evd.future_goals sigma in
let evkmain = Evd.principal_future_goal sigma in
(** Check that the introduced evars are well-typed *)
@@ -1074,7 +1075,11 @@ struct
let refine_casted ?unsafe f = Goal.enter begin fun gl ->
let concl = Goal.concl gl in
let env = Goal.env gl in
- let f h = let (h, c) = f h in with_type env h c concl in
+ let f = { run = fun h ->
+ let Sigma (c, h, p) = f.run h in
+ let sigma, c = with_type env (Sigma.to_evar_map h) c concl in
+ Sigma (c, Sigma.Unsafe.of_evar_map sigma, p)
+ } in
refine ?unsafe f
end
end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 98e1477ff..04ca01ec4 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -487,7 +487,7 @@ module Refine : sig
(** {7 Refinement primitives} *)
- val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic
+ val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
(** In [refine ?unsafe t], [t] is a term with holes under some
[evar_map] context. The term [t] is used as a partial solution
for the current goal (refine is a goal-dependent tactic), the
@@ -503,7 +503,7 @@ module Refine : sig
(** [with_type env sigma c t] ensures that [c] is of type [t]
inserting a coercion if needed. *)
- val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*Constr.t) -> unit tactic
+ val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
(** Like {!refine} except the refined term is coerced to the conclusion of the
current goal. *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 1a3f46039..d7d82111c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -21,6 +21,7 @@ open Util
open Evd
open Equality
open Misctypes
+open Sigma.Notations
DECLARE PLUGIN "extratactics"
@@ -355,7 +356,11 @@ let refine_tac {Glob_term.closure=closure;term=term} =
Pretyping.ltac_uconstrs = closure.Glob_term.untyped;
Pretyping.ltac_idents = closure.Glob_term.idents;
} in
- let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in
+ let update = { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
+ let (sigma, c) = Pretyping.understand_ltac flags env sigma lvar tycon term in
+ Sigma.Unsafe.of_pair (c, sigma)
+ end } in
Tactics.New.refine ~unsafe:false update
end
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ef115aea0..0acaeb44c 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -27,6 +27,7 @@ open Elim
open Equality
open Misctypes
open Tacexpr
+open Sigma.Notations
open Proofview.Notations
let clear hyps = Proofview.V82.tactic (clear hyps)
@@ -457,7 +458,7 @@ let raw_inversion inv_kind id status names =
in
let refined id =
let prf = mkApp (mkVar id, args) in
- Proofview.Refine.refine (fun h -> h, prf)
+ Proofview.Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) }
in
let neqns = List.length realargs in
let as_mode = names != None in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 081170869..1b6ba56e6 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -34,6 +34,7 @@ open Elimschemes
open Environ
open Termops
open Libnames
+open Sigma.Notations
(** Typeclass-based generalized rewriting. *)
@@ -1508,13 +1509,14 @@ let assert_replacing id newt tac =
| (id, b, _) :: rem -> insert_dependent env (id, b, newt) [] after @ rem
in
let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
- Proofview.Refine.refine ~unsafe:false begin fun sigma ->
+ Proofview.Refine.refine ~unsafe:false { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
let sigma, ev = Evarutil.new_evar env' sigma concl in
let sigma, ev' = Evarutil.new_evar env sigma newt in
let map (n, _, _) = if Id.equal n id then ev' else mkVar n in
let (e, _) = destEvar ev in
- sigma, mkEvar (e, Array.map_of_list map nc)
- end
+ Sigma.Unsafe.of_pair (mkEvar (e, Array.map_of_list map nc), sigma)
+ end }
end in
Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
@@ -1533,7 +1535,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
let gls = List.rev (Evd.fold_undefined fold undef []) in
match clause, prf with
| Some id, Some p ->
- let tac = Proofview.Refine.refine ~unsafe:false (fun h -> (h, p)) <*> Proofview.Unsafe.tclNEWGOALS gls in
+ let tac = Proofview.Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in
Proofview.Unsafe.tclEVARS undef <*>
assert_replacing id newt tac
| Some id, None ->
@@ -1543,10 +1545,11 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
Proofview.Unsafe.tclEVARS undef <*>
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let make sigma =
+ let make = { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
let (sigma, ev) = Evarutil.new_evar env sigma newt in
- sigma, mkApp (p, [| ev |])
- in
+ Sigma.Unsafe.of_pair (mkApp (p, [| ev |]), sigma)
+ end } in
Proofview.Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
end
| None, None ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 27166bf48..90e4f8521 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -43,6 +43,7 @@ open Locus
open Locusops
open Misctypes
open Proofview.Notations
+open Sigma.Notations
let nb_prod x =
let rec count n c =
@@ -171,15 +172,16 @@ let _ =
(** This tactic creates a partial proof realizing the introduction rule, but
does not check anything. *)
let unsafe_intro env store (id, c, t) b =
- Proofview.Refine.refine ~unsafe:true begin fun sigma ->
+ Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
let ctx = named_context_val env in
let nctx = push_named_context_val (id, c, t) ctx in
let inst = List.map (fun (id, _, _) -> mkVar id) (named_context env) in
let ninst = mkRel 1 :: inst in
let nb = subst1 (mkVar id) b in
let sigma, ev = new_evar_instance nctx sigma nb ~store ninst in
- sigma, mkNamedLambda_or_LetIn (id, c, t) ev
- end
+ Sigma.Unsafe.of_pair (mkNamedLambda_or_LetIn (id, c, t) ev, sigma)
+ end }
let introduction ?(check=true) id =
Proofview.Goal.enter begin fun gl ->
@@ -206,7 +208,8 @@ let convert_concl ?(check=true) ty k =
let env = Proofview.Goal.env gl in
let store = Proofview.Goal.extra gl in
let conclty = Proofview.Goal.raw_concl gl in
- Proofview.Refine.refine ~unsafe:true begin fun sigma ->
+ Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
let sigma =
if check then begin
ignore (Typing.unsafe_type_of env sigma ty);
@@ -215,8 +218,9 @@ let convert_concl ?(check=true) ty k =
sigma
end else sigma in
let (sigma,x) = Evarutil.new_evar env sigma ~principal:true ~store ty in
- (sigma, if k == DEFAULTcast then x else mkCast(x,k,conclty))
- end
+ let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
+ Sigma.Unsafe.of_pair (ans, sigma)
+ end }
end
let convert_hyp ?(check=true) d =
@@ -227,7 +231,11 @@ let convert_hyp ?(check=true) d =
let store = Proofview.Goal.extra gl in
let sign = convert_hyp check (named_context_val env) sigma d in
let env = reset_with_named_context sign env in
- Proofview.Refine.refine ~unsafe:true (fun sigma -> Evarutil.new_evar env sigma ~principal:true ~store ty)
+ Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
+ let (sigma, c) = Evarutil.new_evar env sigma ~principal:true ~store ty in
+ Sigma.Unsafe.of_pair (c, sigma)
+ end }
end
let convert_concl_no_check = convert_concl ~check:false
@@ -345,9 +353,11 @@ let rename_hyp repl =
let nconcl = subst concl in
let nctx = Environ.val_of_named_context nhyps in
let instance = List.map (fun (id, _, _) -> mkVar id) hyps in
- Proofview.Refine.refine ~unsafe:true begin fun sigma ->
- Evarutil.new_evar_instance nctx sigma nconcl ~store instance
- end
+ Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
+ let (sigma, c) = Evarutil.new_evar_instance nctx sigma nconcl ~store instance in
+ Sigma.Unsafe.of_pair (c, sigma)
+ end }
end
(**************************************************************)
@@ -1047,12 +1057,13 @@ let cut c =
let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in
(** Backward compat: normalize [c]. *)
let c = local_strong whd_betaiota sigma c in
- Proofview.Refine.refine ~unsafe:true begin fun h ->
+ Proofview.Refine.refine ~unsafe:true { run = begin fun h ->
+ let h = Sigma.to_evar_map h in
let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
let (h, x) = Evarutil.new_evar env h c in
let f = mkLambda (Name id, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
- (h, mkApp (f, [|x|]))
- end
+ Sigma.Unsafe.of_pair (mkApp (f, [|x|]), h)
+ end }
else
Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
end
@@ -1700,13 +1711,14 @@ let cut_and_apply c =
| Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
let concl = Proofview.Goal.concl gl in
let env = Tacmach.New.pf_env gl in
- Proofview.Refine.refine begin fun sigma ->
+ Proofview.Refine.refine { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
let typ = mkProd (Anonymous, c2, concl) in
let (sigma, f) = Evarutil.new_evar env sigma typ in
let (sigma, x) = Evarutil.new_evar env sigma c1 in
let ans = mkApp (f, [|mkApp (c, [|x|])|]) in
- (sigma, ans)
- end
+ Sigma.Unsafe.of_pair (ans, sigma)
+ end }
| _ -> error "lapply needs a non-dependent product."
end
@@ -1721,7 +1733,7 @@ let cut_and_apply c =
(* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *)
let new_exact_no_check c =
- Proofview.Refine.refine ~unsafe:true (fun h -> (h, c))
+ Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma (c, h, Sigma.refl) }
let exact_check c =
Proofview.Goal.enter begin fun gl ->
@@ -1763,7 +1775,7 @@ let assumption =
in
if is_same_type then
(Proofview.Unsafe.tclEVARS sigma) <*>
- Proofview.Refine.refine ~unsafe:true (fun h -> (h, mkVar id))
+ Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma (mkVar id, h, Sigma.refl) }
else arec gl only_eq rest
in
let assumption_tac gl =
@@ -1845,9 +1857,11 @@ let clear_body ids =
check_is_type env concl msg
in
check_hyps <*> check_concl <*>
- Proofview.Refine.refine ~unsafe:true begin fun sigma ->
- Evarutil.new_evar env sigma concl
- end
+ Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
+ let (sigma, c) = Evarutil.new_evar env sigma concl in
+ Sigma.Unsafe.of_pair (c, sigma)
+ end }
end
let clear_wildcards ids =
@@ -2419,11 +2433,11 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
let refl = applist (refl, [t;mkVar id]) in
let newenv = insert_before [heq,None,eq;id,body,t] lastlhyp env in
let (sigma,x) = new_evar newenv sigma ~principal:true ~store ccl in
- (sigma,mkNamedLetIn id c t (mkNamedLetIn heq refl eq x))
+ Sigma.Unsafe.of_pair (mkNamedLetIn id c t (mkNamedLetIn heq refl eq x), sigma)
| None ->
let newenv = insert_before [id,body,t] lastlhyp env in
let (sigma,x) = new_evar newenv sigma ~principal:true ~store ccl in
- (sigma,mkNamedLetIn id c t x)
+ Sigma.Unsafe.of_pair (mkNamedLetIn id c t x, sigma)
let letin_tac with_eq id c ty occs =
Proofview.Goal.nf_enter begin fun gl ->
@@ -2496,10 +2510,11 @@ let bring_hyps hyps =
let concl = Tacmach.New.pf_nf_concl gl in
let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
let args = Array.of_list (instance_from_named_context hyps) in
- Proofview.Refine.refine begin fun sigma ->
+ Proofview.Refine.refine { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
let (sigma, ev) = Evarutil.new_evar env sigma newcl in
- (sigma, (mkApp (ev, args)))
- end
+ Sigma.Unsafe.of_pair (mkApp (ev, args), sigma)
+ end }
end
let revert hyps =
@@ -2608,10 +2623,11 @@ let new_generalize_gen_let lconstr =
0 lconstr ((concl, sigma), [])
in
Proofview.Unsafe.tclEVARS sigma <*>
- Proofview.Refine.refine begin fun sigma ->
+ Proofview.Refine.refine { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
let (sigma, ev) = Evarutil.new_evar env sigma newcl in
- (sigma, (applist (ev, args)))
- end
+ Sigma.Unsafe.of_pair ((applist (ev, args)), sigma)
+ end }
end
let generalize_gen lconstr =
@@ -3951,11 +3967,13 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
Tacticals.New.tclTHENLAST)
(Tacticals.New.tclTHENLIST [
Proofview.Unsafe.tclEVARS sigma;
- Proofview.Refine.refine ~unsafe:true (fun sigma ->
+ Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
let b = not with_evars && with_eq != None in
let (sigma,c) = use_bindings env sigma elim b (c0,lbind) t0 in
let t = Retyping.get_type_of env sigma c in
- mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t));
+ mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t)
+ end };
Proofview.(if with_evars then shelve_unifiable else guard_no_unifiable);
if is_arg_pure_hyp
then Tacticals.New.tclTRY (Proofview.V82.tactic (thin [destVar c0]))
@@ -3971,8 +3989,10 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
let env = reset_with_named_context sign env in
Tacticals.New.tclTHENLIST [
Proofview.Unsafe.tclEVARS sigma';
- Proofview.Refine.refine ~unsafe:true (fun sigma ->
- mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None);
+ Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
+ mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None
+ end };
tac
]
end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index ade89fc98..38e6ce0ea 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -430,7 +430,7 @@ end
module New : sig
- val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*constr) -> unit Proofview.tactic
+ val refine : ?unsafe:bool -> constr Sigma.run -> unit Proofview.tactic
(** [refine ?unsafe c] is [Proofview.Refine.refine ?unsafe c]
followed by beta-iota-reduction of the conclusion. *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 805a29e39..439e20a86 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -20,6 +20,7 @@ open Libnames
open Globnames
open Constrintern
open Constrexpr
+open Sigma.Notations
(*i*)
open Decl_kinds
@@ -322,7 +323,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
if not (Option.is_empty term) then
let init_refine =
Tacticals.New.tclTHENLIST [
- Proofview.Refine.refine (fun evm -> evm, Option.get term);
+ Proofview.Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) };
Proofview.Unsafe.tclNEWGOALS gls;
Tactics.New.reduce_after_refine;
]
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 23:29:53 +0000