A reimport of notations now put the corresponding notations again in front.

5 files changed, 80 insertions, 15 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index e8acd767ed..d71b2191a7 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1427,12 +1427,12 @@ let check_parsing_override (scopt,ntn) data = function
   | OnlyParsingData (_,old_data) ->
     let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
     warn_override_if_needed (scopt,ntn) overridden data old_data;
-    None, not overridden
+    None
   | ParsingAndPrintingData (_,on_printing,old_data) ->
     let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
     warn_override_if_needed (scopt,ntn) overridden data old_data;
-    (if on_printing then Some old_data.not_interp else None), not overridden
-  | NoParsingData -> None, false
+    if on_printing then Some old_data.not_interp else None
+  | NoParsingData -> None
 
 let check_printing_override (scopt,ntn) data parsingdata printingdata =
   let parsing_update = match parsingdata with
@@ -1461,15 +1461,15 @@ let update_notation_data (scopt,ntn) use data table =
     try NotationMap.find ntn table with Not_found -> (NoParsingData, []) in
   match use with
   | OnlyParsing ->
-    let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in
-    NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update, exists
+    let printing_update = check_parsing_override (scopt,ntn) data parsingdata in
+    NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update
   | ParsingAndPrinting ->
-    let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in
-    NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update, exists
+    let printing_update = check_parsing_override (scopt,ntn) data parsingdata in
+    NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update
   | OnlyPrinting ->
     let parsingdata, exists = check_printing_override (scopt,ntn) data parsingdata printingdata in
     let printingdata = if exists then printingdata else (true,data) :: printingdata in
-    NotationMap.add ntn (parsingdata, printingdata) table, None, exists
+    NotationMap.add ntn (parsingdata, printingdata) table, None
 
 let rec find_interpretation ntn find = function
   | [] -> raise Not_found
@@ -1742,23 +1742,22 @@ let declare_notation (scopt,ntn) pat df ~use ~also_in_cases_pattern coe deprecat
     not_location = df;
     not_deprecation = deprecation;
   } in
-  let notation_update,printing_update, exists = update_notation_data (scopt,ntn) use notdata sc.notations in
-  if not exists then
-    let sc = { sc with notations = notation_update } in
-    scope_map := String.Map.add scope sc !scope_map;
+  let notation_update,printing_update = update_notation_data (scopt,ntn) use notdata sc.notations in
+  let sc = { sc with notations = notation_update } in
+  scope_map := String.Map.add scope sc !scope_map;
   (* Update the uninterpretation cache *)
   begin match printing_update with
   | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) also_in_cases_pattern pat
   | None -> ()
   end;
-  if not exists && use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat;
+  if use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat;
   (* Register visibility of lonely notations *)
-  if not exists then begin match scopt with
+  begin match scopt with
   | LastLonelyNotation -> scope_stack := LonelyNotationItem ntn :: !scope_stack
   | NotationInScope _ -> ()
   end;
   (* Declare a possible coercion *)
-  if not exists then begin match coe with
+  begin match coe with
    | Some (IsEntryCoercion entry) ->
      let (_,level,_) = level_of_notation ntn in
      let level = match fst ntn with
diff --git a/test-suite/output/bug_10824.out b/test-suite/output/bug_10824.out
new file mode 100644
index 0000000000..4bc5aafbca
--- /dev/null
+++ b/test-suite/output/bug_10824.out
@@ -0,0 +1,4 @@
+!!
+     : Prop
+!!
+     : Prop
diff --git a/test-suite/output/bug_10824.v b/test-suite/output/bug_10824.v
new file mode 100644
index 0000000000..01271f7d61
--- /dev/null
+++ b/test-suite/output/bug_10824.v
@@ -0,0 +1,12 @@
+Module A.
+Notation F := False.
+Notation "!!" := False (at level 100).
+Check False.
+End A.
+
+Module B.
+Notation "!!" := False (at level 100).
+Notation F := False.
+Notation "!!" := False (at level 100).
+Check False.
+End B.
diff --git a/test-suite/output/bug_7443.out b/test-suite/output/bug_7443.out
new file mode 100644
index 0000000000..446ec6a1ad
--- /dev/null
+++ b/test-suite/output/bug_7443.out
@@ -0,0 +1,13 @@
+Literal 1
+     : Type
+[1]
+     : Type
+Literal 1
+     : Type
+[1]
+     : Type
+The command has indeed failed with message:
+The term "1" has type "Datatypes.nat" while it is expected to have type
+ "denote ?t".
+Literal 1
+     : Type
diff --git a/test-suite/output/bug_7443.v b/test-suite/output/bug_7443.v
new file mode 100644
index 0000000000..33f76dbcfa
--- /dev/null
+++ b/test-suite/output/bug_7443.v
@@ -0,0 +1,37 @@
+Inductive type := nat | bool.
+Definition denote (t : type)
+  := match t with
+     | nat => Datatypes.nat
+     | bool => Datatypes.bool
+     end.
+Ltac reify t :=
+  lazymatch eval cbv beta in t with
+  | Datatypes.nat => nat
+  | Datatypes.bool => bool
+  end.
+Notation reify t := (ltac:(let rt := reify t in exact rt)) (only parsing).
+Notation reify_type_of e := (reify ((fun t (_ : t) => t) _ e)) (only parsing).
+Axiom Literal : forall {t}, denote t -> Type.
+Declare Scope foo_scope.
+Delimit Scope foo_scope with foo.
+Open Scope foo_scope.
+Section A.
+  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
+  Check [1]. (* Literal 1 : Type *) (* as expected *)
+  Notation "[ x ]" := (Literal x) : foo_scope.
+  Check @Literal nat 1. (* Incorred: gives Literal 1 : Type when it should give [1]. Fixed by #12950 *)
+  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
+  Check [1]. (* Incorrect: gives Literal 1 : Type when it should give [1]. This is disputable:
+  #12950 considers that giving an only parsing a previous both-parsing-and-printing notation *)
+End A.
+Section B.
+  Notation "[ x ]" := (Literal x) : foo_scope.
+  Check @Literal nat 1. (* [1] : Type *)
+  Fail Check [1]. (* As expected: The command has indeed failed with message:
+  The term "1" has type "Datatypes.nat" while it is expected to have type
+   "denote ?t". *)
+  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
+  Check [1]. (* Should succeed, but instead fails with: Error:
+  The term "1" has type "Datatypes.nat" while it is expected to have type
+  "denote ?t". Fixed by #12950, but previous declaration is cancelled by #12950. *)
+End B.