list, length, app are migrated from List to Datatypes

This allows easier handling of dependencies, for instance RelationClasses
won't have to requires List (which itself requires part of Arith, etc).
One of the underlying ideas is to provide setoid rewriting in Init someday.

Thanks to some notations in List, this change should be fairly transparent
to the user. For instance, one could see that List.length is a notation for
(Datatypes.)length only when doing a Print List.length.

For these notations not to be too intrusive, they are hidden behind an explicit
Export of Datatypes at the end of List. This isn't very pretty, but quite handy.
Notation.ml is patched to stop complaining in the case of reloading the same
Delimit Scope twice.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12452 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 11 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 6ae720fca..39ae27823 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -147,18 +147,23 @@ let delimiters_map = ref Gmap.empty
 
 let declare_delimiters scope key =
   let sc = find_scope scope in
-  if sc.delimiters <> None && Flags.is_verbose () then begin
-    let old = Option.get sc.delimiters in
-    Flags.if_verbose
-      warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
+  let newsc = { sc with delimiters = Some key } in
+  begin match sc.delimiters with
+    | None -> scope_map := Gmap.add scope newsc !scope_map
+    | Some oldkey when oldkey = key -> ()
+    | Some oldkey ->
+	Flags.if_verbose warning
+	  ("Overwritting previous delimiting key "^oldkey^" in scope "^scope);
+	scope_map := Gmap.add scope newsc !scope_map
   end;
-  let sc = { sc with delimiters = Some key } in
-  scope_map := Gmap.add scope sc !scope_map;
-  if Gmap.mem key !delimiters_map then begin
-    let oldsc = Gmap.find key !delimiters_map in
-    Flags.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc)
-  end;
-  delimiters_map := Gmap.add key scope !delimiters_map
+  try
+    let oldscope = Gmap.find key !delimiters_map in
+    if oldscope = scope then ()
+    else begin
+      Flags.if_verbose warning ("Hiding binding of key "^key^" to "^oldscope);
+      delimiters_map := Gmap.add key scope !delimiters_map
+    end
+  with Not_found -> delimiters_map := Gmap.add key scope !delimiters_map
 
 let find_delimiters_scope loc key =
   try Gmap.find key !delimiters_map