diff options
| author | sacerdot | 2004-07-23 14:03:56 +0000 |
|---|---|---|
| committer | sacerdot | 2004-07-23 14:03:56 +0000 |
| commit | a637b4d1cd7876cb6601a303e69ba7847d42d47e (patch) | |
| tree | e8c5944069e733566fc45f800a61aeec599ad033 /parsing | |
| parent | b978cc7cfd16be8d180a175c0b07d4fa03603212 (diff) | |
"Print Setoids" command added.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5968 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 1153a507df..29985d8678 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -579,6 +579,7 @@ GEXTEND Gram | IDENT "Hint"; qid = global -> PrintHint qid | IDENT "Hint"; "*" -> PrintHintDb | IDENT "HintDb"; s = IDENT -> PrintHintDbName s + | IDENT "Setoids" -> PrintSetoids | IDENT "Scopes" -> PrintScopes | IDENT "Scope"; s = IDENT -> PrintScope s | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s |