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