aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.ml
diff options
context:
space:
mode:
authorGravatar monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-03-27 15:01:55 +0000
committerGravatar monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-03-27 15:01:55 +0000
commit2db7c503a14ed44f6e18ffc02d9a2f3f5c4760e7 (patch)
tree72487c2d67c39be43bd652b46bea7bb0a29ed152 /ide/coq.ml
parentb05f75fabd8910c2a69e1f3ce1d93d3c0f72329f (diff)
coqide: efficacite des buts etc...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3795 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.ml')
-rw-r--r--ide/coq.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 881d27bd5..953833439 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -297,6 +297,8 @@ let concl_menu (_,_,concl,_) =
"Decide Equality", "Decide Equality.";
"Simpl", "Simpl.";
+ "Subst", "Subst.";
+
"Red", "Red.";
"Split", "Split.";
"Left", "Left.";