diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ec1e7415b..f656fb32e 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -120,11 +120,6 @@ let test_plurial_form = function "Keywords Variables/Hypotheses/Parameters expect more than one assumption" | _ -> () -let no_coercion loc (c,x) = - if c then Util.user_err_loc - (loc,"no_coercion",str"No coercion allowed here."); - x - (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion |