diff options
Diffstat (limited to 'interp/syntax_def.ml')
| -rw-r--r-- | interp/syntax_def.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index a023462b7..524f6d743 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -82,7 +82,6 @@ let out_pat (ids,ac) = (List.map (fun (id,(sc,typ)) -> (id,sc)) ids,ac) let declare_syntactic_definition local id onlyparse pat = let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () -let pr_global r = pr_global_env Id.Set.empty r let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn) let allow_compat_notations = ref true |