diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-03 09:33:02 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-03 09:33:02 +0000 |
| commit | fbdd94e527d4b3824bffb663a2cef6f300192396 (patch) | |
| tree | c015237f226465d884e8148a1c018d221ff04efd /ide/coq_commands.ml | |
| parent | 8fb7ef8984de20f1b6adbc5f438bd6cfcf4d1ed0 (diff) | |
New command "Add Relation ..." (for the new implementation of setoid_*).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6048 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq_commands.ml')
| -rw-r--r-- | ide/coq_commands.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 1971fb4f0..0176ccf85 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -22,6 +22,7 @@ let commands = [ "Add Rec ML Path"; "Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. "; "Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]."; + "Add Relation"; "Add Setoid"; "Axiom";]; [(* "Back"; *) ]; |