aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenvtac.ml10
-rw-r--r--proofs/evar_refiner.ml4
-rw-r--r--proofs/logic.ml24
-rw-r--r--proofs/logic.mli19
-rw-r--r--proofs/pfedit.ml68
-rw-r--r--proofs/pfedit.mli38
-rw-r--r--proofs/proof.ml51
-rw-r--r--proofs/proof.mli14
-rw-r--r--proofs/proof_global.ml16
-rw-r--r--proofs/proof_global.mli16
-rw-r--r--proofs/proof_type.ml28
-rw-r--r--proofs/proofs.mllib3
-rw-r--r--proofs/redexpr.ml2
-rw-r--r--proofs/refiner.ml17
-rw-r--r--proofs/refiner.mli8
-rw-r--r--proofs/tacmach.ml18
-rw-r--r--proofs/tacmach.mli87
17 files changed, 143 insertions, 280 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index b99cf245fe..4720328893 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -9,7 +9,6 @@
(************************************************************************)
open Util
-open Names
open Constr
open Termops
open Evd
@@ -17,7 +16,6 @@ open EConstr
open Refiner
open Logic
open Reduction
-open Tacmach
open Clenv
(* This function put casts around metavariables whose type could not be
@@ -80,7 +78,7 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
let clenv = { clenv with evd = evd' } in
tclTHEN
(tclEVARS (Evd.clear_metas evd'))
- (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl
+ (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl
end
let clenv_pose_dependent_evars ?(with_evars=false) clenv =
@@ -102,11 +100,11 @@ let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv =
provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
let fail_quick_core_unif_flags = {
- modulo_conv_on_closed_terms = Some full_transparent_state;
+ modulo_conv_on_closed_terms = Some TransparentState.full;
use_metas_eagerly_in_conv_on_closed_terms = false;
use_evars_eagerly_in_conv_on_closed_terms = false;
- modulo_delta = empty_transparent_state;
- modulo_delta_types = full_transparent_state;
+ modulo_delta = TransparentState.empty;
+ modulo_delta_types = TransparentState.full;
check_applied_meta_types = false;
use_pattern_unification = false;
use_meta_bound_pattern_unification = true; (* ? *)
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index c80f370fdc..6c4193c66b 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -10,7 +10,6 @@
open CErrors
open Util
-open Names
open Evd
open Evarutil
open Evarsolve
@@ -38,7 +37,7 @@ let define_and_solve_constraints evk c env evd =
match
List.fold_left
(fun p (pbty,env,t1,t2) -> match p with
- | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2
+ | Success evd -> Evarconv.evar_conv_x TransparentState.full env evd pbty t1 t2
| UnifFailure _ as x -> x) (Success evd)
pbs
with
@@ -53,7 +52,6 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
let flags = {
Pretyping.use_typeclasses = true;
Pretyping.solve_unification_constraints = true;
- Pretyping.use_hook = None;
Pretyping.fail_evar = false;
Pretyping.expand_evars = true } in
try Pretyping.understand_ltac flags
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 4d5711c195..15ba0a704f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -20,7 +20,6 @@ open Environ
open Reductionops
open Inductiveops
open Typing
-open Proof_type
open Type_errors
open Retyping
@@ -62,6 +61,8 @@ let is_unification_error = function
let catchable_exception = function
| CErrors.UserError _ | TypeError _
+ | Proof.OpenProof _
+ (* abstract will call close_proof inside a tactic *)
| Notation.NumeralNotationError _
| RefinerError _ | Indrec.RecursionSchemeError _
| Nametab.GlobalizationError _
@@ -583,12 +584,15 @@ let convert_hyp check sign sigma d =
let prim_refiner r sigma goal =
let env = Goal.V82.env sigma goal in
let cl = Goal.V82.concl sigma goal in
- match r with
- (* Logical rules *)
- | Refine c ->
- let cl = EConstr.Unsafe.to_constr cl in
- check_meta_variables env sigma c;
- let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in
- let sgl = List.rev sgl in
- let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in
- (sgl, sigma)
+ let cl = EConstr.Unsafe.to_constr cl in
+ check_meta_variables env sigma r;
+ let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl r in
+ let sgl = List.rev sgl in
+ let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in
+ (sgl, sigma)
+
+let prim_refiner ~check r sigma goal =
+ if check then
+ with_check (prim_refiner r sigma) goal
+ else
+ prim_refiner r sigma goal
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 2cad278e10..f99076db23 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -13,27 +13,20 @@
open Names
open Constr
open Evd
-open Proof_type
-(** This suppresses check done in [prim_refiner] for the tactic given in
- argument; works by side-effect *)
-
-val with_check : tactic -> tactic
-
-(** [without_check] respectively means:\\
- [Intro]: no check that the name does not exist\\
- [Intro_after]: no check that the name does not exist and that variables in
+(** [check] respectively means:\\
+ [Intro]: check that the name does not exist\\
+ [Intro_after]: check that the name does not exist and that variables in
its type does not escape their scope\\
- [Intro_replacing]: no check that the name does not exist and that
+ [Intro_replacing]: check that the name does not exist and that
variables in its type does not escape their scope\\
[Convert_hyp]:
- no check that the name exist and that its type is convertible\\
+ check that the name exist and that its type is convertible\\
*)
(** The primitive refiner. *)
-val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map
-
+val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal list * evar_map
(** {6 Refiner errors. } *)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e6507332b1..81122e6858 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -26,25 +26,6 @@ let _ = Goptions.declare_bool_option {
let use_unification_heuristics () = !use_unification_heuristics_ref
-let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator =
- let goals = [ (Global.env_of_context hyps , c) ] in
- Proof_global.start_proof sigma id ?pl str goals terminator;
- let env = Global.env () in
- ignore (Proof_global.with_current_proof (fun _ p ->
- match init_tac with
- | None -> p,(true,[])
- | Some tac -> Proof.run_tactic env tac p))
-
-let cook_this_proof p =
- match p with
- | { Proof_global.id;entries=[constr];persistence;universes } ->
- (id,(constr,universes,persistence))
- | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
-
-let cook_proof () =
- cook_this_proof (fst
- (Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)))
-
exception NoSuchGoal
let _ = CErrors.register_handler begin function
| NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
@@ -152,13 +133,19 @@ let next = let n = ref 0 in fun () -> incr n; !n
let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
let evd = Evd.from_ctx ctx in
let terminator = Proof_global.make_terminator (fun _ -> ()) in
- start_proof id goal_kind evd sign typ terminator;
+ let goals = [ (Global.env_of_context sign , typ) ] in
+ Proof_global.start_proof evd id goal_kind goals terminator;
try
let status = by tac in
- let _,(const,univs,_) = cook_proof () in
- Proof_global.discard_current ();
- let univs = UState.demote_seff_univs const univs in
- const, status, univs
+ let open Proof_global in
+ let { entries; universes } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in
+ match entries with
+ | [entry] ->
+ discard_current ();
+ let univs = UState.demote_seff_univs entry universes in
+ entry, status, univs
+ | _ ->
+ CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
with reraise ->
let reraise = CErrors.push reraise in
Proof_global.discard_current ();
@@ -227,36 +214,3 @@ let refine_by_tactic env sigma ty tac =
this hack will work in most cases. *)
let ans = Safe_typing.inline_private_constants_in_constr env ans neff in
ans, sigma
-
-(**********************************************************************)
-(* Support for resolution of evars in tactic interpretation, including
- resolution by application of tactics *)
-
-let implicit_tactic = Summary.ref None ~name:"implicit-tactic"
-
-let declare_implicit_tactic tac = implicit_tactic := Some tac
-
-let clear_implicit_tactic () = implicit_tactic := None
-
-let apply_implicit_tactic tac = (); fun env sigma evk ->
- let evi = Evd.find_undefined sigma evk in
- match snd (evar_source evk sigma) with
- | (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
- when
- Context.Named.equal Constr.equal (Environ.named_context_of_val evi.evar_hyps)
- (Environ.named_context env) ->
- let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in
- (try
- let c = Evarutil.nf_evars_universes sigma (EConstr.Unsafe.to_constr evi.evar_concl) in
- let c = EConstr.of_constr c in
- if Evarutil.has_undefined_evars sigma c then raise Exit;
- let (ans, _, ctx) =
- build_by_tactic env (Evd.evar_universe_context sigma) c tac in
- let sigma = Evd.set_universe_context sigma ctx in
- sigma, EConstr.of_constr ans
- with e when Logic.catchable_exception e -> raise Exit)
- | _ -> raise Exit
-
-let solve_by_implicit_tactic () = match !implicit_tactic with
-| None -> None
-| Some tac -> Some (apply_implicit_tactic tac)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 5feb5bd645..155221947a 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -16,34 +16,6 @@ open Environ
open Decl_kinds
(** {6 ... } *)
-(** [start_proof s str env t hook tac] starts a proof of name [s] and
- conclusion [t]; [hook] is optionally a function to be applied at
- proof end (e.g. to declare the built constructions as a coercion
- or a setoid morphism); init_tac is possibly a tactic to
- systematically apply at initialization time (e.g. to start the
- proof of mutually dependent theorems) *)
-
-val start_proof :
- Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
- ?init_tac:unit Proofview.tactic ->
- Proof_global.proof_terminator -> unit
-
-(** {6 ... } *)
-(** [cook_proof opacity] turns the current proof (assumed completed) into
- a constant with its name, kind and possible hook (see [start_proof]);
- it fails if there is no current proof of if it is not completed;
- it also tells if the guardness condition has to be inferred. *)
-
-val cook_this_proof :
- Proof_global.proof_object ->
- (Id.t *
- (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
-
-val cook_proof : unit ->
- (Id.t *
- (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
-
-(** {6 ... } *)
(** [get_goal_context n] returns the context of the [n]th subgoal of
the current focused proof or raises a [UserError] if there is no
focused proof or if there is no more subgoals *)
@@ -116,13 +88,3 @@ val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.ta
evars solved by side-effects are NOT purged, so that unexpected failures may
occur. Ideally all code using this function should be rewritten in the
monad. *)
-
-(** Declare the default tactic to fill implicit arguments *)
-
-val declare_implicit_tactic : unit Proofview.tactic -> unit
-
-(** To remove the default tactic *)
-val clear_implicit_tactic : unit -> unit
-
-(* Raise Exit if cannot solve *)
-val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 8220949856..6c13c4946a 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -335,28 +335,42 @@ let dependent_start goals =
let number_of_goals = List.length (Proofview.initial_goals pr.entry) in
_focus end_of_stack (Obj.repr ()) 1 number_of_goals pr
-exception UnfinishedProof
-exception HasShelvedGoals
-exception HasGivenUpGoals
-exception HasUnresolvedEvar
+type open_error_reason =
+ | UnfinishedProof
+ | HasShelvedGoals
+ | HasGivenUpGoals
+ | HasUnresolvedEvar
+
+let print_open_error_reason er = let open Pp in match er with
+ | UnfinishedProof ->
+ str "Attempt to save an incomplete proof"
+ | HasShelvedGoals ->
+ str "Attempt to save a proof with shelved goals"
+ | HasGivenUpGoals ->
+ strbrk "Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed."
+ | HasUnresolvedEvar ->
+ strbrk "Attempt to save a proof with existential variables still non-instantiated"
+
+exception OpenProof of Names.Id.t option * open_error_reason
+
let _ = CErrors.register_handler begin function
- | UnfinishedProof -> CErrors.user_err Pp.(str "Some goals have not been solved.")
- | HasShelvedGoals -> CErrors.user_err Pp.(str "Some goals have been left on the shelf.")
- | HasGivenUpGoals -> CErrors.user_err Pp.(str "Some goals have been given up.")
- | HasUnresolvedEvar -> CErrors.user_err Pp.(str "Some existential variables are uninstantiated.")
- | _ -> raise CErrors.Unhandled
-end
+ | OpenProof (pid, reason) ->
+ let open Pp in
+ Option.cata (fun pid ->
+ str " (in proof " ++ Names.Id.print pid ++ str "): ") (mt()) pid ++ print_open_error_reason reason
+ | _ -> raise CErrors.Unhandled
+ end
-let return p =
+let return ?pid (p : t) =
if not (is_done p) then
- raise UnfinishedProof
+ raise (OpenProof(pid, UnfinishedProof))
else if has_shelved_goals p then
- raise HasShelvedGoals
+ raise (OpenProof(pid, HasShelvedGoals))
else if has_given_up_goals p then
- raise HasGivenUpGoals
+ raise (OpenProof(pid, HasGivenUpGoals))
else if has_unresolved_evar p then
(* spiwack: for compatibility with <= 8.3 proof engine *)
- raise HasUnresolvedEvar
+ raise (OpenProof(pid, HasUnresolvedEvar))
else
let p = unfocus end_of_stack_kind p () in
Proofview.return p.proofview
@@ -449,11 +463,10 @@ module V82 = struct
let grab_evars p =
if not (is_done p) then
- raise UnfinishedProof
+ raise (OpenProof(None, UnfinishedProof))
else
{ p with proofview = Proofview.V82.grab p.proofview }
-
(* Main component of vernac command Existential *)
let instantiate_evar n com pr =
let tac =
@@ -491,4 +504,6 @@ let all_goals p =
let set = add goals Goal.Set.empty in
let set = List.fold_left (fun s gs -> let (g1, g2) = gs in add g1 (add g2 set)) set stack in
let set = add shelf set in
- add given_up set
+ let set = add given_up set in
+ let { Evd.it = bgoals ; sigma = bsigma } = V82.background_subgoals p in
+ add bgoals set
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 8cf543557b..aaabea3454 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -89,11 +89,15 @@ val compact : t -> t
Raises [HasShelvedGoals] if some goals are left on the shelf.
Raises [HasGivenUpGoals] if some goals have been given up.
Raises [HasUnresolvedEvar] if some evars have been left undefined. *)
-exception UnfinishedProof
-exception HasShelvedGoals
-exception HasGivenUpGoals
-exception HasUnresolvedEvar
-val return : t -> Evd.evar_map
+type open_error_reason =
+ | UnfinishedProof
+ | HasShelvedGoals
+ | HasGivenUpGoals
+ | HasUnresolvedEvar
+
+exception OpenProof of Names.Id.t option * open_error_reason
+
+val return : ?pid:Names.Id.t -> t -> Evd.evar_map
(*** Focusing actions ***)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 25cf789193..cb4b5759dc 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -176,7 +176,6 @@ let simple_with_current_proof f = with_current_proof (fun t p -> f t p , ())
let compact_the_proof () = simple_with_current_proof (fun _ -> Proof.compact)
-
(* Sets the tactic to be used when a tactic line is closed with [...] *)
let set_endline_tactic tac =
match !pstates with
@@ -416,20 +415,7 @@ let return_proof ?(allow_partial=false) () =
proofs, Evd.evar_universe_context evd
end else
let initial_goals = Proof.initial_goals proof in
- let evd =
- let error s =
- let prf = str " (in proof " ++ Id.print pid ++ str ")" in
- raise (CErrors.UserError(Some "last tactic before Qed",s ++ prf))
- in
- try Proof.return proof with
- | Proof.UnfinishedProof ->
- error(str"Attempt to save an incomplete proof")
- | Proof.HasShelvedGoals ->
- error(str"Attempt to save a proof with shelved goals")
- | Proof.HasGivenUpGoals ->
- error(strbrk"Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed.")
- | Proof.HasUnresolvedEvar->
- error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in
+ let evd = Proof.return ~pid proof in
let eff = Evd.eval_side_effects evd in
let evd = Evd.minimize_universes evd in
(** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 2b04bfab57..e3808bc36d 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -60,14 +60,14 @@ type closed_proof = proof_object * proof_terminator
val make_terminator : (proof_ending -> unit) -> proof_terminator
val apply_terminator : proof_terminator -> proof_ending -> unit
-(** [start_proof id str pl goals terminator] starts a proof of name [id]
- with goals [goals] (a list of pairs of environment and
- conclusion); [str] describes what kind of theorem/definition this
- is (spiwack: for potential printing, I believe is used only by
- closing commands and the xml plugin); [terminator] is used at the
- end of the proof to close the proof. The proof is started in the
- evar map [sigma] (which can typically contain universe
- constraints), and with universe bindings pl. *)
+(** [start_proof id str pl goals terminator] starts a proof of name
+ [id] with goals [goals] (a list of pairs of environment and
+ conclusion); [str] describes what kind of theorem/definition this
+ is; [terminator] is used at the end of the proof to close the proof
+ (e.g. to declare the built constructions as a coercion or a setoid
+ morphism). The proof is started in the evar map [sigma] (which can
+ typically contain universe constraints), and with universe bindings
+ pl. *)
val start_proof :
Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl ->
Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list ->
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
deleted file mode 100644
index 149f30c673..0000000000
--- a/proofs/proof_type.ml
+++ /dev/null
@@ -1,28 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-(** Legacy proof engine. Do not use in newly written code. *)
-
-open Evd
-open Constr
-
-(** This module defines the structure of proof tree and the tactic type. So, it
- is used by [Proof_tree] and [Refiner] *)
-
-type prim_rule =
- | Refine of constr
-
-(** Nowadays, the only rules we'll consider are the primitive rules *)
-
-type rule = prim_rule
-
-type goal = Goal.goal
-
-type tactic = goal sigma -> goal list sigma
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 197f71ca91..dbd5be23ab 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,10 +1,9 @@
Miscprint
Goal
Evar_refiner
-Proof_type
-Logic
Refine
Proof
+Logic
Goal_select
Proof_bullet
Proof_global
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 56ce744bc1..0981584bb5 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -160,7 +160,7 @@ let make_flag env f =
(fun v red -> red_sub red (make_flag_constant v))
f.rConst red
else (* Only rConst *)
- let red = red_add_transparent (red_add red fDELTA) all_opaque in
+ let red = red_add_transparent (red_add red fDELTA) TransparentState.empty in
List.fold_right
(fun v red -> red_add red (make_flag_constant v))
f.rConst red
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index be32aadd91..bce227dabb 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -12,9 +12,10 @@ open Pp
open CErrors
open Util
open Evd
-open Proof_type
open Logic
+type tactic = Proofview.V82.tac
+
module NamedDecl = Context.Named.Declaration
let sig_it x = x.it
@@ -25,16 +26,16 @@ let project x = x.sigma
let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls))
let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
-let refiner pr goal_sigma =
- let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in
+let refiner ~check pr goal_sigma =
+ let (sgl,sigma') = prim_refiner ~check pr goal_sigma.sigma goal_sigma.it in
{ it = sgl; sigma = sigma'; }
(* Profiling refiner *)
-let refiner =
+let refiner ~check =
if Flags.profile then
let refiner_key = CProfile.declare_profile "refiner" in
- CProfile.profile2 refiner_key refiner
- else refiner
+ CProfile.profile2 refiner_key (refiner ~check)
+ else refiner ~check
(*********************)
(* Tacticals *)
@@ -178,9 +179,9 @@ let tclPROGRESS tac ptree =
NOTE: some tactics delete hypothesis and reuse names (induction,
destruct), this is not detected by this tactical. *)
let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
- :Proof_type.goal list Evd.sigma =
+ : Goal.goal list Evd.sigma =
let oldhyps = pf_hyps goal in
- let rslt:Proof_type.goal list Evd.sigma = tac goal in
+ let rslt:Goal.goal list Evd.sigma = tac goal in
let { it = gls; sigma = sigma; } = rslt in
let hyps =
List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 30af6d8e1a..52cbf7658b 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -11,18 +11,18 @@
(** Legacy proof engine. Do not use in newly written code. *)
open Evd
-open Proof_type
open EConstr
(** The refiner (handles primitive rules and high-level tactics). *)
+type tactic = Proofview.V82.tac
val sig_it : 'a sigma -> 'a
val project : 'a sigma -> evar_map
-val pf_env : goal sigma -> Environ.env
-val pf_hyps : goal sigma -> named_context
+val pf_env : Goal.goal sigma -> Environ.env
+val pf_hyps : Goal.goal sigma -> named_context
-val refiner : rule -> tactic
+val refiner : check:bool -> Constr.t -> tactic
(** {6 Tacticals. } *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 231a8fe266..64d7630d55 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -17,9 +17,7 @@ open Evd
open Typing
open Redexpr
open Tacred
-open Proof_type
open Logic
-open Refiner
open Context.Named.Declaration
module NamedDecl = Context.Named.Declaration
@@ -30,7 +28,7 @@ let re_sig it gc = { it = it; sigma = gc; }
(* Operations for handling terms under a local typing context *)
(**************************************************************)
-type tactic = Proof_type.tactic
+type tactic = Proofview.V82.tac
let sig_it = Refiner.sig_it
let project = Refiner.project
@@ -103,20 +101,6 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind
let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls
-(********************************************)
-(* Definition of the most primitive tactics *)
-(********************************************)
-
-let refiner = refiner
-
-let refine_no_check c gl =
- let c = EConstr.Unsafe.to_constr c in
- refiner (Refine c) gl
-
-(* Versions with consistency checks *)
-
-let refine c = with_check (refine_no_check c)
-
(* Pretty-printers *)
open Pp
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 14c83a6802..ef6a1544e4 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -12,85 +12,78 @@ open Names
open Constr
open Environ
open EConstr
-open Proof_type
open Redexpr
open Locus
(** Operations for handling terms under a local typing context. *)
open Evd
-type tactic = Proof_type.tactic;;
+
+type tactic = Proofview.V82.tac
val sig_it : 'a sigma -> 'a
-val project : goal sigma -> evar_map
+val project : Goal.goal sigma -> evar_map
val re_sig : 'a -> evar_map -> 'a sigma
-val pf_concl : goal sigma -> types
-val pf_env : goal sigma -> env
-val pf_hyps : goal sigma -> named_context
-(*i val pf_untyped_hyps : goal sigma -> (Id.t * constr) list i*)
-val pf_hyps_types : goal sigma -> (Id.t * types) list
-val pf_nth_hyp_id : goal sigma -> int -> Id.t
-val pf_last_hyp : goal sigma -> named_declaration
-val pf_ids_of_hyps : goal sigma -> Id.t list
-val pf_global : goal sigma -> Id.t -> evar_map * constr
-val pf_unsafe_type_of : goal sigma -> constr -> types
-val pf_type_of : goal sigma -> constr -> evar_map * types
-val pf_hnf_type_of : goal sigma -> constr -> types
+val pf_concl : Goal.goal sigma -> types
+val pf_env : Goal.goal sigma -> env
+val pf_hyps : Goal.goal sigma -> named_context
+(*i val pf_untyped_hyps : Goal.goal sigma -> (Id.t * constr) list i*)
+val pf_hyps_types : Goal.goal sigma -> (Id.t * types) list
+val pf_nth_hyp_id : Goal.goal sigma -> int -> Id.t
+val pf_last_hyp : Goal.goal sigma -> named_declaration
+val pf_ids_of_hyps : Goal.goal sigma -> Id.t list
+val pf_global : Goal.goal sigma -> Id.t -> evar_map * constr
+val pf_unsafe_type_of : Goal.goal sigma -> constr -> types
+val pf_type_of : Goal.goal sigma -> constr -> evar_map * types
+val pf_hnf_type_of : Goal.goal sigma -> constr -> types
-val pf_get_hyp : goal sigma -> Id.t -> named_declaration
-val pf_get_hyp_typ : goal sigma -> Id.t -> types
+val pf_get_hyp : Goal.goal sigma -> Id.t -> named_declaration
+val pf_get_hyp_typ : Goal.goal sigma -> Id.t -> types
-val pf_get_new_id : Id.t -> goal sigma -> Id.t
+val pf_get_new_id : Id.t -> Goal.goal sigma -> Id.t
-val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr
+val pf_reduction_of_red_expr : Goal.goal sigma -> red_expr -> constr -> evar_map * constr
-val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
+val pf_apply : (env -> evar_map -> 'a) -> Goal.goal sigma -> 'a
val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) ->
- goal sigma -> 'a -> goal sigma * 'b
+ Goal.goal sigma -> 'a -> Goal.goal sigma * 'b
val pf_reduce :
(env -> evar_map -> constr -> constr) ->
- goal sigma -> constr -> constr
+ Goal.goal sigma -> constr -> constr
val pf_e_reduce :
(env -> evar_map -> constr -> evar_map * constr) ->
- goal sigma -> constr -> evar_map * constr
-
-val pf_whd_all : goal sigma -> constr -> constr
-val pf_hnf_constr : goal sigma -> constr -> constr
-val pf_nf : goal sigma -> constr -> constr
-val pf_nf_betaiota : goal sigma -> constr -> constr
-val pf_reduce_to_quantified_ind : goal sigma -> types -> (inductive * EInstance.t) * types
-val pf_reduce_to_atomic_ind : goal sigma -> types -> (inductive * EInstance.t) * types
-val pf_compute : goal sigma -> constr -> constr
+ Goal.goal sigma -> constr -> evar_map * constr
+
+val pf_whd_all : Goal.goal sigma -> constr -> constr
+val pf_hnf_constr : Goal.goal sigma -> constr -> constr
+val pf_nf : Goal.goal sigma -> constr -> constr
+val pf_nf_betaiota : Goal.goal sigma -> constr -> constr
+val pf_reduce_to_quantified_ind : Goal.goal sigma -> types -> (inductive * EInstance.t) * types
+val pf_reduce_to_atomic_ind : Goal.goal sigma -> types -> (inductive * EInstance.t) * types
+val pf_compute : Goal.goal sigma -> constr -> constr
val pf_unfoldn : (occurrences * evaluable_global_reference) list
- -> goal sigma -> constr -> constr
-
-val pf_const_value : goal sigma -> pconstant -> constr
-val pf_conv_x : goal sigma -> constr -> constr -> bool
-val pf_conv_x_leq : goal sigma -> constr -> constr -> bool
-
-(** {6 The most primitive tactics. } *)
-
-val refiner : rule -> tactic
-val refine_no_check : constr -> tactic
+ -> Goal.goal sigma -> constr -> constr
-(** {6 The most primitive tactics with consistency and type checking } *)
-
-val refine : constr -> tactic
+val pf_const_value : Goal.goal sigma -> pconstant -> constr
+val pf_conv_x : Goal.goal sigma -> constr -> constr -> bool
+val pf_conv_x_leq : Goal.goal sigma -> constr -> constr -> bool
(** {6 Pretty-printing functions (debug only). } *)
-val pr_gls : goal sigma -> Pp.t
-val pr_glls : goal list sigma -> Pp.t
+val pr_gls : Goal.goal sigma -> Pp.t
+val pr_glls : Goal.goal list sigma -> Pp.t
[@@ocaml.deprecated "Please move to \"new\" proof engine"]
(** Variants of [Tacmach] functions built with the new proof engine *)
module New : sig
+
val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a
val pf_global : Id.t -> Proofview.Goal.t -> GlobRef.t
+
(** FIXME: encapsulate the level in an existential type. *)
- val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
+ val of_old : (Goal.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
val project : Proofview.Goal.t -> Evd.evar_map
val pf_env : Proofview.Goal.t -> Environ.env
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 01:41:17 +0000