diff options
Diffstat (limited to 'grammar/tacextend.ml4')
| -rw-r--r-- | grammar/tacextend.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index dd00bc19a..aec115b7e 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -189,7 +189,7 @@ let declare_tactic loc s c cl = match cl with let name = mlexpr_of_string name in let tac = (** Special handling of tactics without arguments: such tactics do not do - a Proofview.Goal.enter to compute their arguments. It matters for some + a Proofview.Goal.nf_enter to compute their arguments. It matters for some whole-prof tactics like [shelve_unifiable]. *) if List.is_empty rem then <:expr< fun _ $lid:"ist"$ -> $tac$ >> |