diff options
| author |  Patrick Loiseleur <da+pg-patrl@inf.ed.ac.uk> | 1999-05-17 13:38:16 +0000 |
|---|---|---|
| committer | Patrick Loiseleur <da+pg-patrl@inf.ed.ac.uk> | 1999-05-17 13:38:16 +0000 |
| commit | 3a500cef5174cf878cc38f002d46a400547445b4 (patch) | |
| tree | 469888fbb3fc113ccb3b383d4b473ab0254b7fd7 /coq/coq-syntax.el | |
| parent | 35415802db09738fabb5d3fc04eaf11c0f26249a (diff) | |
several additions, as usual
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index b6507361..c21ed9a2 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -30,6 +30,7 @@ (defvar coq-keywords-goal '( +"Correctness" "Definition" "Fact" "Goal" @@ -52,10 +53,12 @@ (defvar coq-keywords-commands '( +"Add\\s-+ML\\s-+Path" "AddPath" "Begin\\s-+Silent" "Cd" "Check" +"Chapter" "Class" "Coercion" "DelPath" @@ -72,7 +75,18 @@ "Implicit\\s-+Arguments\\s-+Off" "Load" "Local\\s-+Coercion" +"Locate\\s-+File" +"Locate\\s-+Library" +"Locate" "Opaque" +"Print\\s-+Classes" +"Print\\s-+Coercions" +"Print\\s-+Graph" +"Print\\s-+Grammar" +"Print\\s-+Hint" +"Print\\s-+LoadPath" +"Print\\s-+ML\\s-+Path" +"Print\\s-+ML\\s-+Modules" "Print" "Proof" "Pwd" @@ -83,6 +97,9 @@ "Search" "SearchIsos" "Section" +"Show\\s-+Programs" +"Show\\s-+Proof" +"Show\\s-+Script" "Show" "Syntax" "Tactic\\s-+Definition" |