diff options
Diffstat (limited to 'proofs/proof_type.mli')
| -rw-r--r-- | proofs/proof_type.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index a722335d5..5ef9416b3 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -20,7 +20,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 @@ -53,7 +55,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 } |