diff options
Diffstat (limited to 'proofs/proof_type.mli')
| -rw-r--r-- | proofs/proof_type.mli | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 2c57806b51..aab94e4b46 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -12,7 +12,6 @@ open Environ open Evd open Names -open Stamps open Term open Util (*i*) @@ -58,10 +57,6 @@ type prim_rule = { params : Coqast.t list; terms : constr list } -(* A global constraint is a mappings of existential variables - with some extra information for the program tactic *) -type global_constraints = evar_map timestamped - (* The type [goal sigma] is the type of subgoal. It has the following form \begin{verbatim} it = { evar_concl = [the conclusion of the subgoal] @@ -94,7 +89,7 @@ type global_constraints = evar_map timestamped type ['a] (see below the form of a [goal sigma] *) type 'a sigma = { it : 'a ; - sigma : global_constraints } + sigma : evar_map} (*s Proof trees. [ref] = [None] if the goal has still to be proved, |