aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-06 18:34:39 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-06 18:54:04 +0100
commit6ecbc9990a49a0dd51970c7fc8b13f39f02be773 (patch)
tree027928408f8e28263edf98a5bd58cd96d43dffca /proofs
parentd3653c6da5770dfc4d439639b49193e30172763a (diff)
Moving Ltac traces to Tacexpr and Tacinterp.
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proof_type.ml52
-rw-r--r--proofs/proof_type.mli16
-rw-r--r--proofs/proofs.mllib1
3 files changed, 0 insertions, 69 deletions
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