aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof_type.mli
diff options
context:
space:
mode:
authorfilliatr2000-06-21 01:15:42 +0000
committerfilliatr2000-06-21 01:15:42 +0000
commit5378cd45ac34551ea4d265f41b489ff386ea1a49 (patch)
tree655fdd402e962863483cdbb40483fcf8b5ab4892 /proofs/proof_type.mli
parent18ca75a6fbaf2a1238a3a2e36f51f1e1bf1c2c68 (diff)
portage EAuto et Ring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@513 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof_type.mli')
-rw-r--r--proofs/proof_type.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 9c2ac00ae4..a722335d55 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -84,7 +84,7 @@ and tactic = goal sigma -> (goal list sigma * validation)
and validation = (proof_tree list -> proof_tree)
and tactic_arg =
- Command of Coqast.t
+ | Command of Coqast.t
| Constr of constr
| Identifier of identifier
| Integer of int