aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/notation.ml65
-rw-r--r--intf/vernacexpr.mli14
-rw-r--r--library/declaremods.ml40
-rw-r--r--library/declaremods.mli27
-rw-r--r--parsing/g_vernac.ml429
-rw-r--r--printing/ppvernac.ml22
-rw-r--r--test-suite/success/NumberScopes.v62
-rw-r--r--theories/NArith/BinNat.v10
-rw-r--r--theories/Numbers/Integer/BigZ/BigZ.v8
-rw-r--r--theories/Numbers/Integer/BigZ/ZMake.v2
-rw-r--r--theories/Numbers/NatInt/NZBase.v5
-rw-r--r--theories/Numbers/Natural/BigN/BigN.v16
-rw-r--r--theories/Numbers/Natural/BigN/NMake_gen.ml2
-rw-r--r--theories/Numbers/Natural/Peano/NPeano.v2
-rw-r--r--theories/Numbers/Rational/BigQ/BigQ.v5
-rw-r--r--theories/Numbers/Rational/BigQ/QMake.v2
-rw-r--r--theories/PArith/BinPos.v2
-rw-r--r--theories/ZArith/BinInt.v10
-rw-r--r--toplevel/metasyntax.ml2
19 files changed, 163 insertions, 162 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index 8ec578621..a5a6138f6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -546,10 +546,10 @@ end
module ScopeClassMap = Map.Make(ScopeClassOrd)
-let scope_class_map = ref (ScopeClassMap.empty : scope_name ScopeClassMap.t)
+let initial_scope_class_map : scope_name ScopeClassMap.t =
+ ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty
-let _ =
- scope_class_map := ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty
+let scope_class_map = ref initial_scope_class_map
let declare_scope_class sc cl =
scope_class_map := ScopeClassMap.add cl sc !scope_class_map
@@ -584,15 +584,20 @@ let compute_type_scope t =
let compute_scope_of_global ref =
find_scope_class_opt (Some (ScopeRef ref))
-(** When merging scope list, we give priority to the first one (computed
- by substitution), using the second one (user given or earlier automatic)
- as fallback *)
+(** Updating a scope list, thanks to a list of argument classes
+ and the current Bind Scope base. When some current scope
+ have been manually given, the corresponding argument class
+ is emptied below, so this manual scope will be preserved. *)
+
+let update_scope cl sco =
+ match find_scope_class_opt cl with
+ | None -> sco
+ | sco' -> sco'
-let rec merge_scope sc1 sc2 = match sc1, sc2 with
- | [], _ -> sc2
- | _, [] -> sc1
- | Some sc :: sc1, _ :: sc2 -> Some sc :: merge_scope sc1 sc2
- | None :: sc1, sco :: sc2 -> sco :: merge_scope sc1 sc2
+let rec update_scopes cls scl = match cls, scl with
+ | [], _ -> scl
+ | _, [] -> List.map find_scope_class_opt cls
+ | cl :: cls, sco :: scl -> update_scope cl sco :: update_scopes cls scl
let arguments_scope = ref Refmap.empty
@@ -603,7 +608,8 @@ type arguments_scope_discharge_request =
let load_arguments_scope _ (_,(_,r,scl,cls)) =
List.iter (Option.iter check_scope) scl;
- arguments_scope := Refmap.add r (scl,cls) !arguments_scope
+ let initial_stamp = ScopeClassMap.empty in
+ arguments_scope := Refmap.add r (scl,cls,initial_stamp) !arguments_scope
let cache_arguments_scope o =
load_arguments_scope 1 o
@@ -624,9 +630,7 @@ let subst_arguments_scope (subst,(req,r,scl,cls)) =
| Some cl' as ocl' when cl' != cl -> ocl'
| _ -> ocl in
let cls' = List.smartmap subst_cl cls in
- let scl' = merge_scope (List.map find_scope_class_opt cls') scl in
- let scl'' = List.map (Option.map Declaremods.subst_scope) scl' in
- (ArgsScopeNoDischarge,r',scl'',cls')
+ (ArgsScopeNoDischarge,r',scl,cls')
let discharge_arguments_scope (_,(req,r,l,_)) =
if req == ArgsScopeNoDischarge || (isVarRef r && Lib.is_in_section r) then None
@@ -643,10 +647,13 @@ let rebuild_arguments_scope (req,r,l,_) =
(req,r,scs,cls)
| ArgsScopeManual ->
(* Add to the manually given scopes the one found automatically
- for the extra parameters of the section *)
+ for the extra parameters of the section. Discard the classes
+ of the manually given scopes to avoid further re-computations. *)
let l',cls = compute_arguments_scope_full (Global.type_of_global r) in
- let l1,_ = List.chop (List.length l' - List.length l) l' in
- (req,r,l1@l,cls)
+ let nparams = List.length l' - List.length l in
+ let l1 = List.firstn nparams l' in
+ let cls1 = List.firstn nparams cls in
+ (req,r,l1@l,cls1)
type arguments_scope_obj =
arguments_scope_discharge_request * global_reference *
@@ -666,13 +673,23 @@ let is_local local ref = local || isVarRef ref && Lib.is_in_section ref
let declare_arguments_scope_gen req r (scl,cls) =
Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl,cls))
-let declare_arguments_scope local ref scl =
- let req =
- if is_local local ref then ArgsScopeNoDischarge else ArgsScopeManual in
- declare_arguments_scope_gen req ref (scl,[])
+let declare_arguments_scope local r scl =
+ let req = if is_local local r then ArgsScopeNoDischarge else ArgsScopeManual
+ in
+ (* We empty the list of argument classes to disable futher scope
+ re-computations and keep these manually given scopes. *)
+ declare_arguments_scope_gen req r (scl,[])
let find_arguments_scope r =
- try fst (Refmap.find r !arguments_scope)
+ try
+ let (scl,cls,stamp) = Refmap.find r !arguments_scope in
+ let cur_stamp = !scope_class_map in
+ if stamp == cur_stamp then scl
+ else
+ (* Recent changes in the Bind Scope base, we re-compute the scopes *)
+ let scl' = update_scopes cls scl in
+ arguments_scope := Refmap.add r (scl',cls,cur_stamp) !arguments_scope;
+ scl'
with Not_found -> []
let declare_ref_arguments_scope ref =
@@ -959,7 +976,7 @@ let init () =
delimiters_map := String.Map.empty;
notations_key_table := KeyMap.empty;
printing_rules := String.Map.empty;
- scope_class_map := ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty
+ scope_class_map := initial_scope_class_map
let _ =
Summary.declare_summary "symbols"
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index f0f565b53..a780ac0f1 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -230,19 +230,7 @@ type inline =
| DefaultInline
| InlineAt of int
-(** Should we adapt a few scopes during functor application ? *)
-
-type scope_subst = (string * string) list
-
-(** The type of annotations for functor applications *)
-
-type funct_app_annot =
- { ann_inline : inline;
- ann_scope_subst : scope_subst }
-
-type 'a annotated = ('a * funct_app_annot)
-
-type module_ast_inl = module_ast annotated
+type module_ast_inl = module_ast * inline
type module_binder = bool option * lident list * module_ast_inl
(** {6 The type of vernacular expressions} *)
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 15a964792..a5804eb53 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -18,19 +18,7 @@ open Lib
open Mod_subst
open Vernacexpr
-let scope_subst = ref (String.Map.empty : string String.Map.t)
-
-let add_scope_subst sc sc' =
- scope_subst := String.Map.add sc sc' !scope_subst
-
-let register_scope_subst scl =
- List.iter (fun (sc1,sc2) -> add_scope_subst sc1 sc2) scl
-
-let subst_scope sc =
- try String.Map.find sc !scope_subst with Not_found -> sc
-
-let reset_scope_subst () =
- scope_subst := String.Map.empty
+(** {6 Inlining levels} *)
let default_inline () = Some (Flags.get_inline_level ())
@@ -39,8 +27,6 @@ let inl2intopt = function
| InlineAt i -> Some i
| DefaultInline -> default_inline ()
-let inline_annot a = inl2intopt a.ann_inline
-
(* modules and components *)
(* This type is for substitutive lib_objects.
@@ -168,7 +154,7 @@ let funct_entry args m =
let build_subtypes interp_modtype mp args mtys =
List.map
(fun (m,ann) ->
- let inl = inline_annot ann in
+ let inl = inl2intopt ann in
let mte = interp_modtype (Global.env()) m in
let mtb = Mod_typing.translate_module_type (Global.env()) mp inl mte in
let funct_mtb =
@@ -462,7 +448,7 @@ let process_module_seb_binding mbid seb =
process_module_binding mbid (seb2mse seb)
let intern_args interp_modtype (idl,(arg,ann)) =
- let inl = inline_annot ann in
+ let inl = inl2intopt ann in
let lib_dir = Lib.library_dp() in
let env = Global.env() in
let mty = interp_modtype env arg in
@@ -484,7 +470,7 @@ let start_module_ interp_modtype export id args res fs =
let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
let res_entry_o, subtyps = match res with
| Enforce (res,ann) ->
- let inl = inline_annot ann in
+ let inl = inl2intopt ann in
let mte = interp_modtype (Global.env()) res in
let _ = Mod_typing.translate_struct_type_entry (Global.env()) inl mte in
Some (mte,inl), []
@@ -675,7 +661,7 @@ let end_modtype () =
let declare_modtype_ interp_modtype id args mtys (mty,ann) fs =
- let inl = inline_annot ann in
+ let inl = inl2intopt ann in
let mmp = Global.start_modtype id in
let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
let entry = funct_entry arg_entries (interp_modtype (Global.env()) mty) in
@@ -685,10 +671,8 @@ let declare_modtype_ interp_modtype id args mtys (mty,ann) fs =
(* Undo the simulated interactive building of the module type *)
(* and declare the module type as a whole *)
- register_scope_subst ann.ann_scope_subst;
let subst = map_mp mp_from mmp empty_delta_resolver in
let substobjs = (mbids,mmp, subst_objects subst objs) in
- reset_scope_subst ();
Summary.unfreeze_summaries fs;
ignore (add_leaf id (in_modtype (Some (entry,inl), substobjs, sub_mty_l)));
mmp
@@ -731,17 +715,17 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
let env = Global.env() in
let mty_entry_o, subs, inl_res = match res with
| Enforce (mty,ann) ->
- Some (funct interp_modtype mty), [], inline_annot ann
+ Some (funct interp_modtype mty), [], inl2intopt ann
| Check mtys ->
None, build_subtypes interp_modtype mmp arg_entries mtys,
default_inline ()
in
(*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in *)
- let mexpr_entry_o, inl_expr, scl = match mexpr_o with
- | None -> None, default_inline (), []
+ let mexpr_entry_o, inl_expr = match mexpr_o with
+ | None -> None, default_inline ()
| Some (mexpr,ann) ->
- Some (funct interp_modexpr mexpr), inline_annot ann, ann.ann_scope_subst
+ Some (funct interp_modexpr mexpr), inl2intopt ann
in
let entry =
@@ -770,10 +754,8 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
then anomaly (Pp.str "Kernel and Library names do not match");
check_subtypes mp subs;
- register_scope_subst scl;
let subst = map_mp mp_from mp_env resolver in
let substobjs = (mbids,mp_env, subst_objects subst objs) in
- reset_scope_subst ();
ignore (add_leaf id (in_module substobjs));
mmp
@@ -853,7 +835,7 @@ let get_includeself_substobjs env mp1 mbids objs me is_mod inline =
let declare_one_include_inner annot (me,is_mod) =
let env = Global.env() in
let cur_mp = fst (current_prefix ()) in
- let inl = inline_annot annot in
+ let inl = inl2intopt annot in
let (mbids,mp,objs)=
if is_mod then
get_module_substobjs env inl me
@@ -865,10 +847,8 @@ let declare_one_include_inner annot (me,is_mod) =
in
let id = current_mod_id() in
let resolver = Global.add_include me is_mod inl in
- register_scope_subst annot.ann_scope_subst;
let subst = map_mp mp cur_mp resolver in
let substobjs = subst_objects subst objs in
- reset_scope_subst ();
ignore (add_leaf id (in_include substobjs))
let declare_one_include interp_struct (me_ast,annot) =
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 06a4edd84..b76017286 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -16,11 +16,6 @@ open Libobject
open Lib
open Vernacexpr
-(** This modules provides official functions to declare modules and
- module types *)
-
-val subst_scope : string -> string
-
(** {6 Modules } *)
(** [declare_module interp_modtype interp_modexpr id fargs typ expr]
@@ -40,14 +35,14 @@ val declare_module :
(env -> 'modast -> module_struct_entry) ->
(env -> 'modast -> module_struct_entry * bool) ->
Id.t ->
- (Id.t located list * ('modast annotated)) list ->
- ('modast annotated) module_signature ->
- ('modast annotated) list -> module_path
+ (Id.t located list * ('modast * inline)) list ->
+ ('modast * inline) module_signature ->
+ ('modast * inline) list -> module_path
val start_module : (env -> 'modast -> module_struct_entry) ->
bool option -> Id.t ->
- (Id.t located list * ('modast annotated)) list ->
- ('modast annotated) module_signature -> module_path
+ (Id.t located list * ('modast * inline)) list ->
+ ('modast * inline) module_signature -> module_path
val end_module : unit -> module_path
@@ -58,14 +53,14 @@ val end_module : unit -> module_path
val declare_modtype : (env -> 'modast -> module_struct_entry) ->
(env -> 'modast -> module_struct_entry * bool) ->
Id.t ->
- (Id.t located list * ('modast annotated)) list ->
- ('modast annotated) list ->
- ('modast annotated) list ->
+ (Id.t located list * ('modast * inline)) list ->
+ ('modast * inline) list ->
+ ('modast * inline) list ->
module_path
val start_modtype : (env -> 'modast -> module_struct_entry) ->
- Id.t -> (Id.t located list * ('modast annotated)) list ->
- ('modast annotated) list -> module_path
+ Id.t -> (Id.t located list * ('modast * inline)) list ->
+ ('modast * inline) list -> module_path
val end_modtype : unit -> module_path
@@ -110,7 +105,7 @@ val import_module : bool -> module_path -> unit
(** Include *)
val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) ->
- ('struct_expr annotated) list -> unit
+ ('struct_expr * inline) list -> unit
(** {6 ... } *)
(** [iter_all_segments] iterate over all segments, the modules'
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index bc07fe896..450414625 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -455,32 +455,19 @@ GEXTEND Gram
| -> [] ] ]
;
functor_app_annot:
- [ [ IDENT "inline"; "at"; IDENT "level"; i = INT ->
- [InlineAt (int_of_string i)], []
- | IDENT "no"; IDENT "inline" -> [NoInline], []
- | IDENT "scope"; sc1 = IDENT; IDENT "to"; sc2 = IDENT -> [], [sc1,sc2]
- ] ]
- ;
- functor_app_annots:
- [ [ "["; l = LIST1 functor_app_annot SEP ","; "]" ->
- let inl,scs = List.split l in
- let inl = match List.concat inl with
- | [] -> DefaultInline
- | [inl] -> inl
- | _ -> error "Functor application with redundant inline annotations"
- in { ann_inline = inl; ann_scope_subst = List.concat scs }
- | -> { ann_inline = DefaultInline; ann_scope_subst = [] }
+ [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = INT; "]" ->
+ InlineAt (int_of_string i)
+ | "["; IDENT "no"; IDENT "inline"; "]" -> NoInline
+ | -> DefaultInline
] ]
;
module_expr_inl:
- [ [ "!"; me = module_expr ->
- (me, { ann_inline = NoInline; ann_scope_subst = []})
- | me = module_expr; a = functor_app_annots -> (me,a) ] ]
+ [ [ "!"; me = module_expr -> (me,NoInline)
+ | me = module_expr; a = functor_app_annot -> (me,a) ] ]
;
module_type_inl:
- [ [ "!"; me = module_type ->
- (me, { ann_inline = NoInline; ann_scope_subst = []})
- | me = module_type; a = functor_app_annots -> (me,a) ] ]
+ [ [ "!"; me = module_type -> (me,NoInline)
+ | me = module_type; a = functor_app_annot -> (me,a) ] ]
;
(* Module binder *)
module_binder:
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index d8ddb275d..3c4f25880 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -222,21 +222,13 @@ let rec pr_module_ast pr_c = function
pr_module_ast pr_c me1 ++ spc() ++
hov 1 (str"(" ++ pr_module_ast pr_c me2 ++ str")")
-let pr_annot { ann_inline = ann; ann_scope_subst = scl } =
- let sep () = if List.is_empty scl then mt () else str "," in
- if ann == DefaultInline && List.is_empty scl then mt ()
- else
- str " [" ++
- (match ann with
- | DefaultInline -> mt ()
- | NoInline -> str "no inline" ++ sep ()
- | InlineAt i -> str "inline at level " ++ int i ++ sep ()) ++
- prlist_with_sep (fun () -> str ", ")
- (fun (sc1,sc2) -> str ("scope "^sc1^" to "^sc2)) scl ++
- str "]"
-
-let pr_module_ast_inl pr_c (mast,ann) =
- pr_module_ast pr_c mast ++ pr_annot ann
+let pr_inline = function
+ | DefaultInline -> mt ()
+ | NoInline -> str "[no inline]"
+ | InlineAt i -> str "[inline at level " ++ int i ++ str "]"
+
+let pr_module_ast_inl pr_c (mast,inl) =
+ pr_module_ast pr_c mast ++ pr_inline inl
let pr_of_module_type prc = function
| Enforce mty -> str ":" ++ pr_module_ast_inl prc mty
diff --git a/test-suite/success/NumberScopes.v b/test-suite/success/NumberScopes.v
new file mode 100644
index 000000000..ca9457be7
--- /dev/null
+++ b/test-suite/success/NumberScopes.v
@@ -0,0 +1,62 @@
+
+(* We check that various definitions or lemmas have the correct
+ argument scopes, especially the ones created via functor application. *)
+
+Close Scope nat_scope.
+
+Require Import PArith.
+Check (Pos.add 1 2).
+Check (Pos.add_comm 1 2).
+Check (Pos.min_comm 1 2).
+Definition f_pos (x:positive) := x.
+Definition f_pos' (x:Pos.t) := x.
+Check (f_pos 1).
+Check (f_pos' 1).
+
+Require Import ZArith.
+Check (Z.add 1 2).
+Check (Z.add_comm 1 2).
+Check (Z.min_comm 1 2).
+Definition f_Z (x:Z) := x.
+Definition f_Z' (x:Z.t) := x.
+Check (f_Z 1).
+Check (f_Z' 1).
+
+Require Import NArith.
+Check (N.add 1 2).
+Check (N.add_comm 1 2).
+Check (N.min_comm 1 2).
+Definition f_N (x:N) := x.
+Definition f_N' (x:N.t) := x.
+Check (f_N 1).
+Check (f_N' 1).
+
+Require Import NPeano.
+Check (Nat.add 1 2).
+Check (Nat.add_comm 1 2).
+Check (Nat.min_comm 1 2).
+Definition f_nat (x:nat) := x.
+Definition f_nat' (x:Nat.t) := x.
+Check (f_nat 1).
+Check (f_nat' 1).
+
+Require Import BigN.
+Check (BigN.add 1 2).
+Check (BigN.add_comm 1 2).
+Check (BigN.min_comm 1 2).
+Definition f_bigN (x:bigN) := x.
+Check (f_bigN 1).
+
+Require Import BigZ.
+Check (BigZ.add 1 2).
+Check (BigZ.add_comm 1 2).
+Check (BigZ.min_comm 1 2).
+Definition f_bigZ (x:bigZ) := x.
+Check (f_bigZ 1).
+
+Require Import BigQ.
+Check (BigQ.add 1 2).
+Check (BigQ.add_comm 1 2).
+Check (BigQ.min_comm 1 2).
+Definition f_bigQ (x:bigQ) := x.
+Check (f_bigQ 1). \ No newline at end of file
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 5b1e83e6c..61a77bf0e 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -893,11 +893,9 @@ Qed.
(** Instantiation of generic properties of natural numbers *)
-(** The Bind Scope prevents N to stay associated with abstract_scope.
- (TODO FIX) *)
-
-Include NProp. Bind Scope N_scope with N.
-Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+Include NProp
+ <+ UsualMinMaxLogicalProperties
+ <+ UsualMinMaxDecProperties.
(** In generic statements, the predicates [lt] and [le] have been
favored, whereas [gt] and [ge] don't even exist in the abstract
@@ -983,6 +981,8 @@ Qed.
End N.
+Bind Scope N_scope with N.t N.
+
(** Exportation of notations *)
Infix "+" := N.add : N_scope.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index a56f90b08..eca97ace9 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -26,15 +26,13 @@ Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake.
Delimit Scope bigZ_scope with bigZ.
-Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder.
- Include ZMake.Make BigN [scope abstract_scope to bigZ_scope].
- Bind Scope bigZ_scope with t t_.
- Include ZTypeIsZAxioms
+Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder :=
+ ZMake.Make BigN
+ <+ ZTypeIsZAxioms
<+ ZProp [no inline]
<+ HasEqBool2Dec [no inline]
<+ MinMaxLogicalProperties [no inline]
<+ MinMaxDecProperties [no inline].
-End BigZ.
(** For precision concerning the above scope handling, see comment in BigN *)
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 180fe0a96..28c298dbe 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -29,8 +29,6 @@ Module Make (NN:NType) <: ZType.
Definition t := t_.
- Bind Scope abstract_scope with t t_.
-
Definition zero := Pos NN.zero.
Definition one := Pos NN.one.
Definition two := Pos NN.two.
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 62b148294..f073cae89 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -12,11 +12,6 @@ Require Import NZAxioms.
Module Type NZBaseProp (Import NZ : NZDomainSig').
-(** An artificial scope meant to be substituted later *)
-
-Delimit Scope abstract_scope with abstract.
-Bind Scope abstract_scope with t.
-
Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *)
Lemma eq_sym_iff : forall x y, x==y <-> y==x.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 072b75f78..380963cff 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -28,23 +28,13 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
Delimit Scope bigN_scope with bigN.
-Module BigN <: NType <: OrderedTypeFull <: TotalOrder.
- Include NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope].
- Bind Scope bigN_scope with t t'.
- Include NTypeIsNAxioms
+Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
+ NMake.Make Int31Cyclic
+ <+ NTypeIsNAxioms
<+ NProp [no inline]
<+ HasEqBool2Dec [no inline]
<+ MinMaxLogicalProperties [no inline]
<+ MinMaxDecProperties [no inline].
-End BigN.
-
-(** Nota concerning scopes : for the first Include, we cannot bind
- the scope bigN_scope to a type that doesn't exists yet.
- We hence need to explicitely declare the scope substitution.
- For the next Include, the abstract type t (in scope abstract_scope)
- gets substituted to concrete BigN.t (in scope bigN_scope),
- and the corresponding argument scope are fixed automatically.
-*)
(** Notations about [BigN] *)
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index b941ed48f..b28ce15b9 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -138,8 +138,6 @@ pr
pr "";
pr " Definition t := t'.";
pr "";
- pr " Bind Scope abstract_scope with t t'.";
- pr "";
pr " (** * A generic toolbox for building and deconstructing [t] *)";
pr "";
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index a510b3ae2..5e36916b9 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -800,6 +800,8 @@ Include NProp
End Nat.
+Bind Scope nat_scope with Nat.t nat.
+
(** [Nat] contains an [order] tactic for natural numbers *)
(** Note that [Nat.order] is domain-agnostic: it will not prove
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index a2bc5e266..50c90757a 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -38,9 +38,8 @@ End BigN_BigZ.
Delimit Scope bigQ_scope with bigQ.
Module BigQ <: QType <: OrderedTypeFull <: TotalOrder.
- Include QMake.Make BigN BigZ BigN_BigZ [scope abstract_scope to bigQ_scope].
- Bind Scope bigQ_scope with t t_.
- Include !QProperties <+ HasEqBool2Dec
+ Include QMake.Make BigN BigZ BigN_BigZ
+ <+ !QProperties <+ HasEqBool2Dec
<+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
Ltac order := Private_Tac.order.
End BigQ.
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index a13bb5114..167be6d70 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -39,8 +39,6 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
Definition t := t_.
- Bind Scope abstract_scope with t t_.
-
(** Specification with respect to [QArith] *)
Local Open Scope Q_scope.
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index be5858718..aa065e3c5 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1840,6 +1840,8 @@ Qed.
End Pos.
+Bind Scope positive_scope with Pos.t positive.
+
(** Exportation of notations *)
Infix "+" := Pos.add : positive_scope.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index eeec9042f..6948d420a 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1153,11 +1153,9 @@ Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _.
Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
-(** The Bind Scope prevents Z to stay associated with abstract_scope.
- (TODO FIX) *)
-
-Include ZProp. Bind Scope Z_scope with Z.
-Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+Include ZProp
+ <+ UsualMinMaxLogicalProperties
+ <+ UsualMinMaxDecProperties.
(** In generic statements, the predicates [lt] and [le] have been
favored, whereas [gt] and [ge] don't even exist in the abstract
@@ -1277,6 +1275,8 @@ Qed.
End Z.
+Bind Scope Z_scope with Z.t Z.
+
(** Re-export Notations *)
Infix "+" := Z.add : Z_scope.
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 0c95201d2..8ec699c71 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1280,7 +1280,7 @@ let subst_scope_command (subst,(scope,o as x)) = match o with
| ScopeClasses cl ->
let cl' = List.map_filter (subst_scope_class subst) cl in
let cl' =
- if Int.equal (List.length cl) (List.length cl') && List.for_all2 (==) cl cl' then cl
+ if List.for_all2eq (==) cl cl' then cl
else cl' in
scope, ScopeClasses cl'
| _ -> x
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 19:06:30 +0000