diff options
Diffstat (limited to 'contrib/romega/g_romega.ml4')
| -rw-r--r-- | contrib/romega/g_romega.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/romega/g_romega.ml4 b/contrib/romega/g_romega.ml4 index 386f7f28..7cfc50f8 100644 --- a/contrib/romega/g_romega.ml4 +++ b/contrib/romega/g_romega.ml4 @@ -10,6 +10,6 @@ open Refl_omega -TACTIC EXTEND ROmega - [ "ROmega" ] -> [ total_reflexive_omega_tactic ] +TACTIC EXTEND romelga + [ "romega" ] -> [ total_reflexive_omega_tactic ] END |