diff options
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 6b989b6ba..65e046fb8 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -146,7 +146,7 @@ let mkTacCase with_evar = function (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) | [ElimOnIdent id,(None,None)],None,None -> - TacCase (with_evar,(CRef (Ident id),NoBindings)) + TacCase (with_evar,(CRef (Ident id,None),NoBindings)) | ic -> if List.exists (function (ElimOnAnonHyp _,_) -> true | _ -> false) (pi1 ic) then |