diff options
| author | herbelin | 2003-04-11 08:55:56 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-11 08:55:56 +0000 |
| commit | 7006a5d550c63540c2a4a820ccfd76a09b8d54bd (patch) | |
| tree | 2e785f147f3a42b10b20e9c3eeab870cff5e5728 /interp/syntax_def.ml | |
| parent | a04706bd19e8ebc06fdb9c9f7eebd049edd4a9f3 (diff) | |
Ajout option 'Local' à Infix et Notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3915 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/syntax_def.ml')
| -rw-r--r-- | interp/syntax_def.ml | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index d24ac4673f..69094507d2 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -31,7 +31,7 @@ let _ = Summary.declare_summary let add_syntax_constant kn c = syntax_table := KNmap.add kn c !syntax_table -let load_syntax_constant i ((sp,kn),(c,onlyparse)) = +let load_syntax_constant i ((sp,kn),(local,c,onlyparse)) = if Nametab.exists_cci sp then errorlabstrm "cache_syntax_constant" (pr_id (basename sp) ++ str " already exists"); @@ -46,10 +46,14 @@ let open_syntax_constant i ((sp,kn),c) = let cache_syntax_constant d = load_syntax_constant 1 d -let subst_syntax_constant ((sp,kn),subst,(c,onlyparse)) = - (subst_aconstr subst c,onlyparse) +let subst_syntax_constant ((sp,kn),subst,(local,c,onlyparse)) = + (local,subst_aconstr subst c,onlyparse) -let classify_syntax_constant (_,c) = Substitute c +let classify_syntax_constant (_,(local,_,_ as o)) = + if local then Dispose else Substitute o + +let export_syntax_constant (local,_,_ as o) = + if local then None else Some o let (in_syntax_constant, out_syntax_constant) = declare_object {(default_object "SYNTAXCONSTANT") with @@ -58,10 +62,10 @@ let (in_syntax_constant, out_syntax_constant) = open_function = open_syntax_constant; subst_function = subst_syntax_constant; classify_function = classify_syntax_constant; - export_function = (fun x -> Some x) } + export_function = export_syntax_constant } -let declare_syntactic_definition id onlyparse c = - let _ = add_leaf id (in_syntax_constant (c,onlyparse)) in () +let declare_syntactic_definition local id onlyparse c = + let _ = add_leaf id (in_syntax_constant (local,c,onlyparse)) in () let rec set_loc loc _ a = map_aconstr_with_binders_loc loc (fun id e -> (id,e)) (set_loc loc) () a |