diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-28 14:33:06 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-28 14:33:06 +0000 |
| commit | 8d595e0592972d29ccf4cbbd6b61f6b1aa06a952 (patch) | |
| tree | 9b4874910cc4fe7cff170e034d0b6369fea287f6 /proofs/proof_type.ml | |
| parent | 603111ab1d61d87640222dec37e02199f2f8cb52 (diff) | |
Modifs de presentation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@520 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index eaebd6b99..462b038a1 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -7,8 +7,8 @@ open Term open Util (*i*) -(*This module defines the structure of proof tree and the tactic type. So, it - is used by Proof_tree and Refiner*) +(* This module defines the structure of proof tree and the tactic type. So, it + is used by Proof_tree and Refiner *) type bindOcc = | Dep of identifier @@ -17,7 +17,9 @@ type bindOcc = type 'a substitution = (bindOcc * 'a) list -type pf_status = Complete_proof | Incomplete_proof +type pf_status = + | Complete_proof + | Incomplete_proof type prim_rule_name = | Intro @@ -50,7 +52,7 @@ type evar_declarations = ctxtty evar_map with some extra information for the program tactic *) type global_constraints = evar_declarations timestamped -(*Signature useful to define the tactic type*) +(* Signature useful to define the tactic type *) type 'a sigma = { it : 'a ; sigma : global_constraints } |