diff options
| author | clrenard | 2001-11-12 15:56:10 +0000 |
|---|---|---|
| committer | clrenard | 2001-11-12 15:56:10 +0000 |
| commit | ecb17841e955ca888010d72876381a86cdcf09ad (patch) | |
| tree | 4c6c24f6ce5a8221f8632fceb0f6717948cdca8d /proofs/proof_type.mli | |
| 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.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, |