aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/printers.mllib1
-rw-r--r--printing/printer.ml2
-rw-r--r--proofs/proof.ml28
-rw-r--r--proofs/proofs.mllib1
-rw-r--r--proofs/proofview.ml117
-rw-r--r--proofs/proofview.mli41
-rw-r--r--proofs/refine.ml122
-rw-r--r--proofs/refine.mli37
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/rewrite.ml6
-rw-r--r--tactics/tactics.ml32
-rw-r--r--tactics/tactics.mli2
-rw-r--r--toplevel/classes.ml2
14 files changed, 209 insertions, 186 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 7710033db..c46f6b72a 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -184,6 +184,7 @@ Proof_errors
Logic_monad
Proofview_monad
Proofview
+Refine
Proof
Proof_global
Pfedit
diff --git a/printing/printer.ml b/printing/printer.ml
index b89005887..2e67fa5ff 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -50,7 +50,7 @@ let pr_lconstr_core goal_concl_style env sigma t =
let pr_lconstr_env env = pr_lconstr_core false env
let pr_constr_env env = pr_constr_core false env
-let _ = Hook.set Proofview.Refine.pr_constr pr_constr_env
+let _ = Hook.set Refine.pr_constr pr_constr_env
let pr_lconstr_goal_style_env env = pr_lconstr_core true env
let pr_constr_goal_style_env env = pr_constr_core true env
diff --git a/proofs/proof.ml b/proofs/proof.ml
index b604fde4e..86af420dc 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -334,22 +334,24 @@ let compact p =
(*** Tactics ***)
let run_tactic env tac pr =
+ let open Proofview.Notations in
let sp = pr.proofview in
- let (_,tacticced_proofview,(status,to_shelve,give_up),info_trace) =
- Proofview.apply env tac sp
+ let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in
+ let tac =
+ tac >>= fun () ->
+ Proofview.tclEVARMAP >>= fun sigma ->
+ (* Already solved goals are not to be counted as shelved. Nor are
+ they to be marked as unresolvable. *)
+ let retrieved = undef sigma (List.rev (Evd.future_goals sigma)) in
+ let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in
+ Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+ Proofview.tclUNIT retrieved
in
- let sigma = Proofview.return tacticced_proofview in
- (* Already solved goals are not to be counted as shelved. Nor are
- they to be marked as unresolvable. *)
- let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in
- let retrieved = undef (List.rev (Evd.future_goals sigma)) in
- let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in
- let proofview =
- List.fold_left
- Proofview.Unsafe.mark_as_goal
- tacticced_proofview
- retrieved
+ let (retrieved,proofview,(status,to_shelve,give_up),info_trace) =
+ Proofview.apply env tac sp
in
+ let sigma = Proofview.return proofview in
+ let shelf = (undef sigma pr.shelf)@retrieved@(undef sigma to_shelve) in
let given_up = pr.given_up@give_up in
let proofview = Proofview.Unsafe.reset_future_goals proofview in
{ pr with proofview ; shelf ; given_up },(status,info_trace)
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 08556d62e..236d47932 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -5,6 +5,7 @@ Proof_using
Proof_errors
Logic
Proofview
+Refine
Proof
Proof_global
Redexpr
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index f42a60d9d..20be02e76 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -901,7 +901,7 @@ module Unsafe = struct
let reset_future_goals p =
{ p with solution = Evd.reset_future_goals p.solution }
- let mark_as_goal_evm evd content =
+ let mark_as_goal evd content =
let info = Evd.find evd content in
let info =
{ info with Evd.evar_source = match info.Evd.evar_source with
@@ -911,8 +911,7 @@ module Unsafe = struct
let info = Typeclasses.mark_unresolvable info in
Evd.add evd content info
- let mark_as_goal p gl =
- { p with solution = mark_as_goal_evm p.solution gl }
+ let advance = advance
end
@@ -1075,118 +1074,6 @@ end
-(** {6 The refine tactic} *)
-
-module Refine =
-struct
-
- let extract_prefix env info =
- let ctx1 = List.rev (Environ.named_context env) in
- let ctx2 = List.rev (Evd.evar_context info) in
- let rec share l1 l2 accu = match l1, l2 with
- | d1 :: l1, d2 :: l2 ->
- if d1 == d2 then share l1 l2 (d1 :: accu)
- else (accu, d2 :: l2)
- | _ -> (accu, l2)
- in
- share ctx1 ctx2 []
-
- let typecheck_evar ev env sigma =
- let info = Evd.find sigma ev in
- (** Typecheck the hypotheses. *)
- let type_hyp (sigma, env) decl =
- let t = get_type decl in
- let evdref = ref sigma in
- let _ = Typing.e_sort_of env evdref t in
- let () = match decl with
- | LocalAssum _ -> ()
- | LocalDef (_,body,_) -> Typing.e_check env evdref body t
- in
- (!evdref, Environ.push_named decl env)
- in
- let (common, changed) = extract_prefix env info in
- let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in
- let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
- (** Typecheck the conclusion *)
- let evdref = ref sigma in
- let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
- !evdref
-
- let typecheck_proof c concl env sigma =
- let evdref = ref sigma in
- let () = Typing.e_check env evdref c concl in
- !evdref
-
- let (pr_constrv,pr_constr) =
- Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
-
- let refine ?(unsafe = true) f = Goal.enter { Goal.enter = begin fun gl ->
- let sigma = Goal.sigma gl in
- let sigma = Sigma.to_evar_map sigma in
- let env = Goal.env gl in
- let concl = Goal.concl gl in
- (** Save the [future_goals] state to restore them after the
- refinement. *)
- let prev_future_goals = Evd.future_goals sigma in
- let prev_principal_goal = Evd.principal_future_goal sigma in
- (** Create the refinement term *)
- 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 *)
- let fold accu ev = typecheck_evar ev env accu in
- let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in
- (** Check that the refined term is typesafe *)
- let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in
- (** Check that the goal itself does not appear in the refined term *)
- let _ =
- if not (Evarutil.occur_evar_upto sigma gl.Goal.self c) then ()
- else Pretype_errors.error_occur_check env sigma gl.Goal.self c
- in
- (** Proceed to the refinement *)
- let sigma = match evkmain with
- | None -> Evd.define gl.Goal.self c sigma
- | Some evk ->
- let id = Evd.evar_ident gl.Goal.self sigma in
- let sigma = Evd.define gl.Goal.self c sigma in
- match id with
- | None -> sigma
- | Some id -> Evd.rename evk id sigma
- in
- (** Restore the [future goals] state. *)
- let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in
- (** Select the goals *)
- let comb = undefined sigma (CList.rev evs) in
- let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in
- let open Proof in
- InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
- Pv.modify (fun ps -> { ps with solution = sigma; comb; })
- end }
-
- (** Useful definitions *)
-
- let with_type env evd c t =
- let my_type = Retyping.get_type_of env evd c in
- let j = Environ.make_judge c my_type in
- let (evd,j') =
- Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
- in
- evd , j'.Environ.uj_val
-
- let refine_casted ?unsafe f = Goal.enter { Goal.enter = begin fun gl ->
- let concl = Goal.concl gl in
- let env = Goal.env gl 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
-
-
-
(** {6 Trace} *)
module Trace = struct
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 20f67f258..6bc2e9a0e 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -406,7 +406,13 @@ module Unsafe : sig
(** Give an evar the status of a goal (changes its source location
and makes it unresolvable for type classes. *)
- val mark_as_goal : proofview -> Evar.t -> proofview
+ val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map
+
+ (** [advance sigma g] returns [Some g'] if [g'] is undefined and is
+ the current avatar of [g] (for instance [g] was changed by [clear]
+ into [g']). It returns [None] if [g] has been (partially)
+ solved. *)
+ val advance : Evd.evar_map -> Evar.t -> Evar.t option
end
(** This module gives access to the innards of the monad. Its use is
@@ -491,39 +497,6 @@ module Goal : sig
end
-(** {6 The refine tactic} *)
-
-module Refine : sig
-
- (** Printer used to print the constr which refine refines. *)
- val pr_constr :
- (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t
-
- (** {7 Refinement primitives} *)
-
- 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
- new holes created by [t] become the new subgoals. Exceptions
- raised during the interpretation of [t] are caught and result in
- tactic failures. If [unsafe] is [false] (default is [true]) [t] is
- type-checked beforehand. *)
-
- (** {7 Helper functions} *)
-
- val with_type : Environ.env -> Evd.evar_map ->
- Term.constr -> Term.types -> Evd.evar_map * Term.constr
- (** [with_type env sigma c t] ensures that [c] is of type [t]
- inserting a coercion if needed. *)
-
- 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. *)
-
-end
-
-
(** {6 Trace} *)
module Trace : sig
diff --git a/proofs/refine.ml b/proofs/refine.ml
new file mode 100644
index 000000000..db0b26f7e
--- /dev/null
+++ b/proofs/refine.ml
@@ -0,0 +1,122 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Pp
+open Util
+open Proofview_monad
+open Sigma.Notations
+open Proofview.Notations
+open Context.Named.Declaration
+
+let extract_prefix env info =
+ let ctx1 = List.rev (Environ.named_context env) in
+ let ctx2 = List.rev (Evd.evar_context info) in
+ let rec share l1 l2 accu = match l1, l2 with
+ | d1 :: l1, d2 :: l2 ->
+ if d1 == d2 then share l1 l2 (d1 :: accu)
+ else (accu, d2 :: l2)
+ | _ -> (accu, l2)
+ in
+ share ctx1 ctx2 []
+
+let typecheck_evar ev env sigma =
+ let info = Evd.find sigma ev in
+ (** Typecheck the hypotheses. *)
+ let type_hyp (sigma, env) decl =
+ let t = get_type decl in
+ let evdref = ref sigma in
+ let _ = Typing.e_sort_of env evdref t in
+ let () = match decl with
+ | LocalAssum _ -> ()
+ | LocalDef (_,body,_) -> Typing.e_check env evdref body t
+ in
+ (!evdref, Environ.push_named decl env)
+ in
+ let (common, changed) = extract_prefix env info in
+ let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in
+ let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
+ (** Typecheck the conclusion *)
+ let evdref = ref sigma in
+ let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
+ !evdref
+
+let typecheck_proof c concl env sigma =
+ let evdref = ref sigma in
+ let () = Typing.e_check env evdref c concl in
+ !evdref
+
+let (pr_constrv,pr_constr) =
+ Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
+
+let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl ->
+ let gl = Proofview.Goal.assume gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let sigma = Sigma.to_evar_map sigma in
+ let env = Proofview.Goal.env gl in
+ let concl = Proofview.Goal.concl gl in
+ (** Save the [future_goals] state to restore them after the
+ refinement. *)
+ let prev_future_goals = Evd.future_goals sigma in
+ let prev_principal_goal = Evd.principal_future_goal sigma in
+ (** Create the refinement term *)
+ 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 *)
+ let fold accu ev = typecheck_evar ev env accu in
+ let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in
+ (** Check that the refined term is typesafe *)
+ let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in
+ (** Check that the goal itself does not appear in the refined term *)
+ let self = Proofview.Goal.goal gl in
+ let _ =
+ if not (Evarutil.occur_evar_upto sigma self c) then ()
+ else Pretype_errors.error_occur_check env sigma self c
+ in
+ (** Proceed to the refinement *)
+ let sigma = match evkmain with
+ | None -> Evd.define self c sigma
+ | Some evk ->
+ let id = Evd.evar_ident self sigma in
+ let sigma = Evd.define self c sigma in
+ match id with
+ | None -> sigma
+ | Some id -> Evd.rename evk id sigma
+ in
+ (** Restore the [future goals] state. *)
+ let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in
+ (** Select the goals *)
+ let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in
+ let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
+ let trace () = Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)) in
+ Proofview.Trace.name_tactic trace (Proofview.tclUNIT ()) >>= fun () ->
+ Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+ Proofview.Unsafe.tclSETGOALS comb
+end }
+
+(** Useful definitions *)
+
+let with_type env evd c t =
+ let my_type = Retyping.get_type_of env evd c in
+ let j = Environ.make_judge c my_type in
+ let (evd,j') =
+ Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
+ in
+ evd , j'.Environ.uj_val
+
+let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl ->
+ let gl = Proofview.Goal.assume gl in
+ let concl = Proofview.Goal.concl gl in
+ let env = Proofview.Goal.env gl 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 }
diff --git a/proofs/refine.mli b/proofs/refine.mli
new file mode 100644
index 000000000..17c7e28ca
--- /dev/null
+++ b/proofs/refine.mli
@@ -0,0 +1,37 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Proofview
+
+(** {6 The refine tactic} *)
+
+(** Printer used to print the constr which refine refines. *)
+val pr_constr :
+ (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t
+
+(** {7 Refinement primitives} *)
+
+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
+ new holes created by [t] become the new subgoals. Exceptions
+ raised during the interpretation of [t] are caught and result in
+ tactic failures. If [unsafe] is [false] (default is [true]) [t] is
+ type-checked beforehand. *)
+
+(** {7 Helper functions} *)
+
+val with_type : Environ.env -> Evd.evar_map ->
+ Term.constr -> Term.types -> Evd.evar_map * Term.constr
+(** [with_type env sigma c t] ensures that [c] is of type [t]
+ inserting a coercion if needed. *)
+
+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 0cc796886..23aa8dcb4 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -370,7 +370,7 @@ let refine_tac ist simple c =
let expected_type = Pretyping.OfType concl in
let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in
let update = { run = fun sigma -> c.delayed env sigma } in
- let refine = Proofview.Refine.refine ~unsafe:false update in
+ let refine = Refine.refine ~unsafe:false update in
if simple then refine
else refine <*>
Tactics.New.reduce_after_refine <*>
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 6841ab0ec..89c6beb32 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -459,7 +459,7 @@ let raw_inversion inv_kind id status names =
in
let refined id =
let prf = mkApp (mkVar id, args) in
- Proofview.Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) }
+ 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 67d21886b..4c06550d4 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1539,7 +1539,7 @@ let assert_replacing id newt tac =
| d :: rem -> insert_dependent env (LocalAssum (get_id d, newt)) [] after @ rem
in
let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
- Proofview.Refine.refine ~unsafe:false { run = begin fun sigma ->
+ Refine.refine ~unsafe:false { run = begin fun sigma ->
let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in
let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in
let map d =
@@ -1568,7 +1568,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress 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 { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in
+ let tac = 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 ->
@@ -1582,7 +1582,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma newt in
Sigma (mkApp (p, [| ev |]), sigma, q)
end } in
- Proofview.Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
+ Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
end }
| None, None ->
Proofview.Unsafe.tclEVARS undef <*>
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ffe10d81c..7ae178af5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -163,7 +163,7 @@ let _ =
does not check anything. *)
let unsafe_intro env store decl b =
let open Context.Named.Declaration in
- Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+ Refine.refine ~unsafe:true { run = begin fun sigma ->
let ctx = named_context_val env in
let nctx = push_named_context_val decl ctx in
let inst = List.map (mkVar % get_id) (named_context env) in
@@ -199,7 +199,7 @@ 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 { run = begin fun sigma ->
+ Refine.refine ~unsafe:true { run = begin fun sigma ->
let Sigma ((), sigma, p) =
if check then begin
let sigma = Sigma.to_evar_map sigma in
@@ -222,7 +222,7 @@ 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 { run = begin fun sigma ->
+ Refine.refine ~unsafe:true { run = begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true ~store ty
end }
end }
@@ -345,7 +345,7 @@ let rename_hyp repl =
let nconcl = subst concl in
let nctx = Environ.val_of_named_context nhyps in
let instance = List.map (mkVar % get_id) hyps in
- Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+ Refine.refine ~unsafe:true { run = begin fun sigma ->
Evarutil.new_evar_instance nctx sigma nconcl ~store instance
end }
end }
@@ -1070,7 +1070,7 @@ 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 = if normalize_cut then local_strong whd_betaiota sigma c else c in
- Proofview.Refine.refine ~unsafe:true { run = begin fun h ->
+ Refine.refine ~unsafe:true { run = begin fun h ->
let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
let Sigma (x, h, q) = Evarutil.new_evar env h c in
let f = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
@@ -1736,7 +1736,7 @@ 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 { run = begin fun sigma ->
+ Refine.refine { run = begin fun sigma ->
let typ = mkProd (Anonymous, c2, concl) in
let Sigma (f, sigma, p) = Evarutil.new_evar env sigma typ in
let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c1 in
@@ -1757,7 +1757,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 { run = fun h -> Sigma.here c h }
+ Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h }
let exact_check c =
Proofview.Goal.s_enter { s_enter = begin fun gl ->
@@ -1808,7 +1808,7 @@ let assumption =
in
if is_same_type then
(Proofview.Unsafe.tclEVARS sigma) <*>
- Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h }
+ Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h }
else arec gl only_eq rest
in
let assumption_tac = { enter = begin fun gl ->
@@ -1893,7 +1893,7 @@ let clear_body ids =
check_is_type env concl msg
in
check_hyps <*> check_concl <*>
- Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+ Refine.refine ~unsafe:true { run = begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true concl
end }
end }
@@ -1950,7 +1950,7 @@ let apply_type newcl args =
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let store = Proofview.Goal.extra gl in
- Proofview.Refine.refine { run = begin fun sigma ->
+ Refine.refine { run = begin fun sigma ->
let newcl = nf_betaiota (Sigma.to_evar_map sigma) newcl (* As in former Logic.refine *) in
let Sigma (ev, sigma, p) =
Evarutil.new_evar env sigma ~principal:true ~store newcl in
@@ -1971,7 +1971,7 @@ 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 (Context.Named.to_instance hyps) in
- Proofview.Refine.refine { run = begin fun sigma ->
+ Refine.refine { run = begin fun sigma ->
let Sigma (ev, sigma, p) =
Evarutil.new_evar env sigma ~principal:true ~store newcl in
Sigma (mkApp (ev, args), sigma, p)
@@ -2671,7 +2671,7 @@ let new_generalize_gen_let lconstr =
0 lconstr (concl, sigma, [])
in
let tac =
- Proofview.Refine.refine { run = begin fun sigma ->
+ Refine.refine { run = begin fun sigma ->
let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true newcl in
Sigma ((applist (ev, args)), sigma, p)
end }
@@ -3325,7 +3325,7 @@ let mk_term_eq env sigma ty t ty' t' =
let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
let open Context.Rel.Declaration in
- Proofview.Refine.refine { run = begin fun sigma ->
+ Refine.refine { run = begin fun sigma ->
let eqslen = List.length eqs in
(* Abstract by the "generalized" hypothesis equality proof if necessary. *)
let abshypeq, abshypt =
@@ -4126,7 +4126,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
(* and destruct has side conditions first *)
Tacticals.New.tclTHENLAST)
(Tacticals.New.tclTHENLIST [
- Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+ Refine.refine ~unsafe:true { run = begin fun sigma ->
let b = not with_evars && with_eq != None in
let Sigma (c, sigma, p) = use_bindings env sigma elim b (c0,lbind) t0 in
let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in
@@ -4150,7 +4150,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
let env = reset_with_named_context sign env in
let tac =
Tacticals.New.tclTHENLIST [
- Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+ Refine.refine ~unsafe:true { run = begin fun sigma ->
mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None
end };
tac
@@ -4795,6 +4795,6 @@ module New = struct
{onhyps=None; concl_occs=AllOccurrences }
let refine ?unsafe c =
- Proofview.Refine.refine ?unsafe c <*>
+ Refine.refine ?unsafe c <*>
reduce_after_refine
end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 26ea01769..4c4a96ec0 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -431,7 +431,7 @@ end
module New : sig
val refine : ?unsafe:bool -> constr Sigma.run -> unit Proofview.tactic
- (** [refine ?unsafe c] is [Proofview.Refine.refine ?unsafe c]
+ (** [refine ?unsafe c] is [Refine.refine ?unsafe c]
followed by beta-iota-reduction of the conclusion. *)
val reduce_after_refine : unit Proofview.tactic
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 0a83c49c8..4bf0450d2 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -330,7 +330,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 { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) };
+ 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-11-30 21:40:50 +0000