diff options
| author | letouzey | 2011-02-11 16:54:18 +0000 |
|---|---|---|
| committer | letouzey | 2011-02-11 16:54:18 +0000 |
| commit | 483e36a76c4a31a1711a4602be45f66e7f46760f (patch) | |
| tree | 6a490563e2a55d14e91da600f3843b8fc0b09552 /interp/notation.ml | |
| parent | 1e1bc1952499bf3528810f2b3e6efad76ab843d0 (diff) | |
Annotations at functor applications:
- The experimental syntax "<30>F M" is transformed into "F M [inline at level 30]"
- The earlier syntax !F X should now be written "F X [no inline]"
(note that using ! is still possible for compatibility)
- A new annotation "F M [scope foo_scope to bar_scope]" allow to substitute
foo_scope by bar_scope in all arguments scope of objects in F.
BigN and BigZ are cleaned from the zillions of Arguments Scope used earlier.
Arguments scope for lemmas are fixed for instances of Numbers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13839 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 86a5155374..6be016c180 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -435,7 +435,8 @@ open Classops let class_scope_map = ref (Gmap.empty : (cl_typ,scope_name) Gmap.t) -let _ = Gmap.add CL_SORT "type_scope" Gmap.empty +let _ = + class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty let declare_class_scope sc cl = class_scope_map := Gmap.add cl sc !class_scope_map @@ -479,7 +480,9 @@ let cache_arguments_scope o = load_arguments_scope 1 o let subst_arguments_scope (subst,(req,r,scl)) = - (ArgsScopeNoDischarge,fst (subst_global subst r),scl) + let r' = fst (subst_global subst r) in + let scl' = list_smartmap (Option.smartmap Declaremods.subst_scope) scl in + (ArgsScopeNoDischarge,r',scl') let discharge_arguments_scope (_,(req,r,l)) = if req = ArgsScopeNoDischarge or (isVarRef r & Lib.is_in_section r) then None @@ -527,6 +530,7 @@ let declare_ref_arguments_scope ref = let t = Global.type_of_global ref in declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope t) + (********************************) (* Encoding notations as string *) |