aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/printers.mllib1
-rw-r--r--intf/tacexpr.mli12
-rw-r--r--proofs/proof_type.ml52
-rw-r--r--proofs/proof_type.mli16
-rw-r--r--proofs/proofs.mllib1
-rw-r--r--tactics/tacinterp.ml2
-rw-r--r--tactics/tacinterp.mli2
-rw-r--r--tactics/tacsubst.ml2
-rw-r--r--tactics/tacsubst.mli4
-rw-r--r--toplevel/cerrors.ml2
-rw-r--r--toplevel/himsg.ml22
-rw-r--r--toplevel/himsg.mli2
12 files changed, 35 insertions, 83 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 39e4b1cdb..34bde1ac2 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -174,7 +174,6 @@ Implicit_quantifiers
Constrintern
Modintern
Constrextern
-Proof_type
Goal
Miscprint
Logic
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index f2a567c00..b1dc174d4 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -394,3 +394,15 @@ type tactic_arg =
type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
+
+(** Traces *)
+
+type ltac_call_kind =
+ | LtacMLCall of glob_tactic_expr
+ | LtacNotationCall of KerName.t
+ | LtacNameCall of ltac_constant
+ | LtacAtomCall of glob_atomic_tactic_expr
+ | LtacVarCall of Id.t * glob_tactic_expr
+ | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map
+
+type ltac_trace = (Loc.t * ltac_call_kind) list
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
deleted file mode 100644
index dd2c7b253..000000000
--- a/proofs/proof_type.ml
+++ /dev/null
@@ -1,52 +0,0 @@
-(************************************************************************)
-(* 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 *)
-(************************************************************************)
-
-(*i*)
-open Evd
-open Names
-open Term
-open Tacexpr
-open Glob_term
-open Nametab
-open Misctypes
-(*i*)
-
-(* This module defines the structure of proof tree and the tactic type. So, it
- is used by Proof_tree and Refiner *)
-
-(** Types of goals, tactics, rules ... *)
-
-type goal = Goal.goal
-
-type tactic = goal sigma -> goal list sigma
-
-type prim_rule =
- | Cut of bool * bool * Id.t * types
- | FixRule of Id.t * int * (Id.t * int * constr) list * int
- | Cofix of Id.t * (Id.t * constr) list * int
- | Refine of constr
- | Thin of Id.t list
- | Move of Id.t * Id.t move_location
-
-(** Nowadays, the only rules we'll consider are the primitive rules *)
-
-type rule = prim_rule
-
-(** Ltac traces *)
-
-type ltac_call_kind =
- | LtacMLCall of glob_tactic_expr
- | LtacNotationCall of KerName.t
- | LtacNameCall of ltac_constant
- | LtacAtomCall of glob_atomic_tactic_expr
- | LtacVarCall of Id.t * glob_tactic_expr
- | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map
-
-type ltac_trace = (Loc.t * ltac_call_kind) list
-
-let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index aa05f58ab..b4c9dae2a 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -57,19 +57,3 @@ type rule = prim_rule
type goal = Goal.goal
type tactic = goal sigma -> goal list sigma
-
-(** Ltac traces *)
-
-(** TODO: Move those definitions somewhere sensible *)
-
-type ltac_call_kind =
- | LtacMLCall of glob_tactic_expr
- | LtacNotationCall of KerName.t
- | LtacNameCall of ltac_constant
- | LtacAtomCall of glob_atomic_tactic_expr
- | LtacVarCall of Id.t * glob_tactic_expr
- | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map
-
-type ltac_trace = (Loc.t * ltac_call_kind) list
-
-val ltac_trace_info : ltac_trace Exninfo.t
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 1bd701cb9..47a637575 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -2,7 +2,6 @@ Miscprint
Goal
Evar_refiner
Proof_using
-Proof_type
Proof_errors
Logic
Proofview
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bf5f9ddc8..82252610a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -44,6 +44,8 @@ open Sigma.Notations
open Proofview.Notations
open Context.Named.Declaration
+let ltac_trace_info = Tacsubst.ltac_trace_info
+
let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
let Val.Dyn (t, _) = v in
match Val.eq t (val_tag wit) with
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index c5da3494c..31327873e 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -14,6 +14,8 @@ open Genarg
open Redexpr
open Misctypes
+val ltac_trace_info : ltac_trace Exninfo.t
+
module Value :
sig
type t = Val.t
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 55941c1ca..17cb8ad19 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -18,6 +18,8 @@ open Genredexpr
open Patternops
open Pretyping
+let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
+
(** Substitution of tactics at module closing time *)
(** For generic arguments, we declare and store substitutions
diff --git a/tactics/tacsubst.mli b/tactics/tacsubst.mli
index c1bf27257..8b686c5ce 100644
--- a/tactics/tacsubst.mli
+++ b/tactics/tacsubst.mli
@@ -11,6 +11,10 @@ open Mod_subst
open Genarg
open Misctypes
+(** TODO: Move those definitions somewhere sensible *)
+
+val ltac_trace_info : ltac_trace Exninfo.t
+
(** Substitution of tactics at module closing time *)
val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 600683d35..91ef45393 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -120,7 +120,7 @@ let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc,
let err = Errors.make_anomaly msg in
Util.iraise (err, info)
in
- let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in
+ let ltac_trace = Exninfo.get info Tacsubst.ltac_trace_info in
let loc = Option.default Loc.ghost (Loc.get_loc info) in
match ltac_trace with
| None -> e
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index de7ec61c8..1af09dd84 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1247,9 +1247,9 @@ let explain_reduction_tactic_error = function
let is_defined_ltac trace =
let rec aux = function
- | (_, Proof_type.LtacNameCall f) :: tail ->
+ | (_, Tacexpr.LtacNameCall f) :: tail ->
not (Tacenv.is_ltac_for_ml_tactic f)
- | (_, Proof_type.LtacAtomCall _) :: tail ->
+ | (_, Tacexpr.LtacAtomCall _) :: tail ->
false
| _ :: tail -> aux tail
| [] -> false in
@@ -1258,17 +1258,17 @@ let is_defined_ltac trace =
let explain_ltac_call_trace last trace loc =
let calls = last :: List.rev_map snd trace in
let pr_call ck = match ck with
- | Proof_type.LtacNotationCall kn -> quote (KerName.print kn)
- | Proof_type.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
- | Proof_type.LtacMLCall t ->
+ | Tacexpr.LtacNotationCall kn -> quote (KerName.print kn)
+ | Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
+ | Tacexpr.LtacMLCall t ->
quote (Pptactic.pr_glob_tactic (Global.env()) t)
- | Proof_type.LtacVarCall (id,t) ->
+ | Tacexpr.LtacVarCall (id,t) ->
quote (Nameops.pr_id id) ++ strbrk " (bound to " ++
Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
- | Proof_type.LtacAtomCall te ->
+ | Tacexpr.LtacAtomCall te ->
quote (Pptactic.pr_glob_tactic (Global.env())
(Tacexpr.TacAtom (Loc.ghost,te)))
- | Proof_type.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) ->
+ | Tacexpr.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) ->
quote (pr_glob_constr_env (Global.env()) c) ++
(if not (Id.Map.is_empty vars) then
strbrk " (with " ++
@@ -1282,7 +1282,7 @@ let explain_ltac_call_trace last trace loc =
| [] -> mt ()
| _ ->
let kind_of_last_call = match List.last calls with
- | Proof_type.LtacConstrInterp _ -> ", last term evaluation failed."
+ | Tacexpr.LtacConstrInterp _ -> ", last term evaluation failed."
| _ -> ", last call failed."
in
hov 0 (str "In nested Ltac calls to " ++
@@ -1290,9 +1290,9 @@ let explain_ltac_call_trace last trace loc =
let skip_extensions trace =
let rec aux = function
- | (_,Proof_type.LtacNameCall f as tac) :: _
+ | (_,Tacexpr.LtacNameCall f as tac) :: _
when Tacenv.is_ltac_for_ml_tactic f -> [tac]
- | (_,(Proof_type.LtacNotationCall _ | Proof_type.LtacMLCall _) as tac)
+ | (_,(Tacexpr.LtacNotationCall _ | Tacexpr.LtacMLCall _) as tac)
:: _ -> [tac]
| t :: tail -> t :: aux tail
| [] -> [] in
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 3ef98380b..50bbd15c6 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -37,7 +37,7 @@ val explain_reduction_tactic_error :
Tacred.reduction_tactic_error -> std_ppcmds
val extract_ltac_trace :
- Proof_type.ltac_trace -> Loc.t -> std_ppcmds option * Loc.t
+ Tacexpr.ltac_trace -> Loc.t -> std_ppcmds option * Loc.t
val explain_module_error : Modops.module_typing_error -> std_ppcmds
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 12:26:42 +0000