Merge branch 'v8.6'

4 files changed, 39 insertions, 31 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8520bd5d8..786f15b40 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1051,6 +1051,15 @@ let find_pattern_variable = function
   | Ident (loc,id) -> id
   | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x))
 
+let check_duplicate loc fields =
+  let eq (ref1, _) (ref2, _) = eq_reference ref1 ref2 in
+  let dups = List.duplicates eq fields in
+  match dups with
+  | [] -> ()
+  | (r, _) :: _ ->
+    user_err ~loc (str "This record defines several times the field " ++
+      pr_reference r ++ str ".")
+
 (** [sort_fields ~complete loc fields completer] expects a list
     [fields] of field assignments [f = e1; g = e2; ...], where [f, g]
     are fields of a record and [e1] are "values" (either terms, when
@@ -1084,6 +1093,7 @@ let sort_fields ~complete loc fields completer =
           try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id)
           with Not_found ->
             anomaly (str "Environment corruption for records") in
+        let () = check_duplicate loc fields in
         let (end_index,    (* one past the last field index *)
              first_field_index,  (* index of the first field of the record *)
              proj_list)    (* list of projections *)
diff --git a/interp/notation.ml b/interp/notation.ml
index 29d1f01eb..1bd1bc7d5 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -556,15 +556,13 @@ let ntpe_eq t1 t2 = match t1, t2 with
 | NtnTypeBinderList, NtnTypeBinderList -> true
 | (NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList), _ -> false
 
-
-let vars_eq (id1, (sc1, tp1)) (id2, (sc2, tp2)) =
-  Id.equal id1 id2 &&
+let var_attributes_eq (_, (sc1, tp1)) (_, (sc2, tp2)) =
   pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
   ntpe_eq tp1 tp2
 
 let interpretation_eq (vars1, t1) (vars2, t2) =
-  List.equal vars_eq vars1 vars2 &&
-  Notation_ops.eq_notation_constr t1 t2
+  List.equal var_attributes_eq vars1 vars2 &&
+  Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2
 
 let exists_notation_in_scope scopt ntn r =
   let scope = match scopt with Some s -> s | None -> default_scope in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 2f3ebcc9b..fca1c7904 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -47,62 +47,62 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
     | GHole _ | GSort _ | GLetIn _), _
       -> false
 
-let rec eq_notation_constr t1 t2 = match t1, t2 with
+let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
 | NRef gr1, NRef gr2 -> eq_gr gr1 gr2
-| NVar id1, NVar id2 -> Id.equal id1 id2
+| NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2)
 | NApp (t1, a1), NApp (t2, a2) ->
-  eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2
+  (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2
 | NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *)
 | NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) ->
-  Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
-  eq_notation_constr u1 u2 && b1 == b2
+  Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
+  (eq_notation_constr vars) u1 u2 && b1 == b2
 | NLambda (na1, t1, u1), NLambda (na2, t2, u2) ->
-  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+  Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
 | NProd (na1, t1, u1), NProd (na2, t2, u2) ->
-  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+  Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
 | NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) ->
-  Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
-  eq_notation_constr u1 u2
+  Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
+  (eq_notation_constr vars) u1 u2
 | NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) ->
-  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+  Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
 | NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *)
   let eqpat (p1, t1) (p2, t2) =
     List.equal cases_pattern_eq p1 p2 &&
-    eq_notation_constr t1 t2
+    (eq_notation_constr vars) t1 t2
   in
   let eqf (t1, (na1, o1)) (t2, (na2, o2)) =
     let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in
-    eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
+    (eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
   in
-  Option.equal eq_notation_constr o1 o2 &&
+  Option.equal (eq_notation_constr vars) o1 o2 &&
   List.equal eqf r1 r2 &&
   List.equal eqpat p1 p2
 | NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) ->
   List.equal Name.equal nas1 nas2 &&
   Name.equal na1 na2 &&
-  Option.equal eq_notation_constr o1 o2 &&
-  eq_notation_constr t1 t2 &&
-  eq_notation_constr u1 u2
+  Option.equal (eq_notation_constr vars) o1 o2 &&
+  (eq_notation_constr vars) t1 t2 &&
+  (eq_notation_constr vars) u1 u2
 | NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
-  eq_notation_constr t1 t2 &&
+  (eq_notation_constr vars) t1 t2 &&
   Name.equal na1 na2 &&
-  Option.equal eq_notation_constr o1 o2 &&
-  eq_notation_constr u1 u2 &&
-  eq_notation_constr r1 r2
+  Option.equal (eq_notation_constr vars) o1 o2 &&
+  (eq_notation_constr vars) u1 u2 &&
+  (eq_notation_constr vars) r1 r2
 | NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *)
   let eq (na1, o1, t1) (na2, o2, t2) =
     Name.equal na1 na2 &&
-    Option.equal eq_notation_constr o1 o2 &&
-    eq_notation_constr t1 t2
+    Option.equal (eq_notation_constr vars) o1 o2 &&
+    (eq_notation_constr vars) t1 t2
   in
   Array.equal Id.equal ids1 ids2 &&
   Array.equal (List.equal eq) ts1 ts2 &&
-  Array.equal eq_notation_constr us1 us2 &&
-  Array.equal eq_notation_constr rs1 rs2
+  Array.equal (eq_notation_constr vars) us1 us2 &&
+  Array.equal (eq_notation_constr vars) rs1 rs2
 | NSort s1, NSort s2 ->
   Miscops.glob_sort_eq s1 s2
 | NCast (t1, c1), NCast (t2, c2) ->
-  eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2
+  (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
   | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
   | NRec _ | NSort _ | NCast _), _ -> false
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 854e222e3..4ebd3ddd8 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -12,7 +12,7 @@ open Glob_term
 
 (** {5 Utilities about [notation_constr]} *)
 
-val eq_notation_constr : notation_constr -> notation_constr -> bool
+val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool
 
 (** Substitution of kernel names in interpretation data                *)