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 9b21837d8..23e4ba621 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -104,7 +104,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) = (id,n,CProdN(loc,bl,ty)) let mk_cofix_tac (loc,id,bl,ann,ty) = - let _ = option_map (fun (aloc,_) -> + let _ = Option.map (fun (aloc,_) -> Util.user_err_loc (aloc,"Constr:mk_cofix_tac", Pp.str"Annotation forbidden in cofix expression")) ann in |