diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-09 20:05:36 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-09 20:05:36 +0000 |
| commit | e03541b7092e136edc78335cb178c0217dd48bc5 (patch) | |
| tree | 08ecb04e49ecfbba5416e6a62e5268d1dc804bbf /interp | |
| parent | c4aedb6ef3e605dc61b937f0e7fa8f596bd7e2be (diff) | |
Deactivation of (intrusive) printing of abbreviations from non-imported modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12487 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/syntax_def.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 1330a3689..b0e27f04e 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -36,10 +36,7 @@ let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) = errorlabstrm "cache_syntax_constant" (pr_id (basename sp) ++ str " already exists"); add_syntax_constant kn pat; - Nametab.push_syndef (Nametab.Until i) sp kn; - if not onlyparse then - (* Declare it to be used as long name *) - Notation.declare_uninterpretation (Notation.SynDefRule kn) pat + Nametab.push_syndef (Nametab.Until i) sp kn let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = Nametab.push_syndef (Nametab.Exactly i) sp kn; |