diff options
author | clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-12 15:56:10 +0000 |
---|---|---|
committer | clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-12 15:56:10 +0000 |
commit | ecb17841e955ca888010d72876381a86cdcf09ad (patch) | |
tree | 4c6c24f6ce5a8221f8632fceb0f6717948cdca8d /proofs/proof_type.ml | |
parent | 2f611e10fb3dc42fc00d80b1e087fa33f6fc846e (diff) |
Suppression des stamps et donc des *_constraints
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2186 85f007b7-540e-0410-9357-904b9bb8a0f7
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 81c57e539..9965488c9 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, |