diff options
Diffstat (limited to 'contrib/rtauto/g_rtauto.ml4')
| -rw-r--r-- | contrib/rtauto/g_rtauto.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/rtauto/g_rtauto.ml4 b/contrib/rtauto/g_rtauto.ml4 index ee47d0b02..4cbe84368 100644 --- a/contrib/rtauto/g_rtauto.ml4 +++ b/contrib/rtauto/g_rtauto.ml4 @@ -10,7 +10,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -TACTIC EXTEND Rtauto - [ "Rtauto" ] -> [ Refl_tauto.rtauto_tac ] +TACTIC EXTEND rtauto + [ "rtauto" ] -> [ Refl_tauto.rtauto_tac ] END |