diff options
Diffstat (limited to 'contrib/subtac/g_eterm.ml4')
| -rw-r--r-- | contrib/subtac/g_eterm.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/subtac/g_eterm.ml4 b/contrib/subtac/g_eterm.ml4 index 7b4bc31b4..095e5fafc 100644 --- a/contrib/subtac/g_eterm.ml4 +++ b/contrib/subtac/g_eterm.ml4 @@ -19,8 +19,8 @@ open Eterm -TACTIC EXTEND Eterm - [ "Eterm" ] -> [ +TACTIC EXTEND eterm + [ "eterm" ] -> [ (fun gl -> let evm = Tacmach.project gl and t = Tacmach.pf_concl gl in Eterm.etermtac (evm, t) gl) ] |