diff options
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 81c57e5390..9965488c9f 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -9,7 +9,6 @@ open Environ open Evd open Names -open Stamps open Term open Util (*i*) @@ -55,14 +54,10 @@ 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 - (* Signature useful to define the tactic type *) type 'a sigma = { it : 'a ; - sigma : global_constraints } + sigma : evar_map } (*s Proof trees. [ref] = [None] if the goal has still to be proved, |