7 files changed, 26 insertions, 6 deletions
diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v
index 931d753521..6ddad8f1c9 100644
--- a/user-contrib/Ltac2/Notations.v
+++ b/user-contrib/Ltac2/Notations.v
@@ -593,6 +593,8 @@ Ltac2 Notation "typeclasses_eauto" "bfs" n(opt(tactic(0)))
 
 Ltac2 Notation typeclasses_eauto := typeclasses_eauto.
 
+Ltac2 Notation "unify" x(constr) y(constr) := Std.unify x y.
+
 (** Congruence *)
 
 Ltac2 f_equal0 () := ltac1:(f_equal).
diff --git a/user-contrib/Ltac2/Std.v b/user-contrib/Ltac2/Std.v
index b69a95faf3..3675df9f75 100644
--- a/user-contrib/Ltac2/Std.v
+++ b/user-contrib/Ltac2/Std.v
@@ -259,3 +259,5 @@ Ltac2 @ external new_auto : debug -> int option -> (unit -> constr) list -> iden
 Ltac2 @ external eauto : debug -> int option -> int option -> (unit -> constr) list -> ident list option -> unit := "ltac2" "tac_eauto".
 
 Ltac2 @ external typeclasses_eauto : strategy option -> int option -> ident list option -> unit := "ltac2" "tac_typeclasses_eauto".
+
+Ltac2 @ external unify : constr -> constr -> unit := "ltac2" "tac_unify".
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 7af530ab0f..6aa31e9c91 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -675,12 +675,12 @@ let perform_notation syn st =
     CAst.make ~loc @@ CTacLet (false, bnd, syn.synext_exp)
   in
   let rule = Pcoq.Production.make rule (act mk) in
-  let lev = match syn.synext_lev with
+  let pos = match syn.synext_lev with
   | None -> None
-  | Some lev -> Some (string_of_int lev)
+  | Some lev -> Some (Gramlib.Gramext.Level (string_of_int lev))
   in
-  let rule = (lev, None, [rule]) in
-  ([Pcoq.ExtendRule (Pltac.ltac2_expr, {Pcoq.pos=None; data=[rule]})], st)
+  let rule = (None, None, [rule]) in
+  ([Pcoq.ExtendRule (Pltac.ltac2_expr, {Pcoq.pos; data=[rule]})], st)
 
 let ltac2_notation =
   Pcoq.create_grammar_command "ltac2-notation" perform_notation
@@ -754,7 +754,15 @@ let register_notation ?deprecation ?(local = false) tkn lev body = match tkn, le
   let ids = List.fold_left fold Id.Set.empty entries in
   (* Globalize so that names are absolute *)
   let body = Tac2intern.globalize ids body in
-  let lev = match lev with Some _ -> lev | None -> Some 5 in
+  let lev = match lev with
+  | Some n ->
+    let () =
+      if n < 0 || n > 6 then
+        user_err (str "Notation levels must range between 0 and 6")
+    in
+    lev
+  | None -> Some 5
+  in
   let ext = {
     synext_tok = tkn;
     synext_exp = body;
diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index 206f4df19d..0171ddfcf8 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -468,7 +468,7 @@ let polymorphic ((n, t) : type_scheme) : mix_type_scheme =
 let warn_not_unit =
   CWarnings.create ~name:"not-unit" ~category:"ltac"
     (fun (env, t) ->
-      strbrk "The following expression should have type unit but has type " ++
+      strbrk "This expression should have type unit but has type " ++
       pr_glbtype env t ++ str ".")
 
 let warn_redundant_clause =
diff --git a/user-contrib/Ltac2/tac2stdlib.ml b/user-contrib/Ltac2/tac2stdlib.ml
index 895b6d3975..c7dfb3e69e 100644
--- a/user-contrib/Ltac2/tac2stdlib.ml
+++ b/user-contrib/Ltac2/tac2stdlib.ml
@@ -572,3 +572,7 @@ end
 let () = define_prim3 "tac_typeclasses_eauto" (option strategy) (option int) (option (list ident)) begin fun str n dbs ->
   Tac2tactics.typeclasses_eauto str n dbs
 end
+
+let () = define_prim2 "tac_unify" constr constr begin fun x y ->
+  Tac2tactics.unify x y
+end
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml
index 54f5a2cf68..a30f6e7945 100644
--- a/user-contrib/Ltac2/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -414,6 +414,8 @@ let typeclasses_eauto strategy depth dbs =
   in
   Class_tactics.typeclasses_eauto ~only_classes ?strategy ~depth dbs
 
+let unify x y = Tactics.unify x y
+
 (** Inversion *)
 
 let inversion knd arg pat ids =
diff --git a/user-contrib/Ltac2/tac2tactics.mli b/user-contrib/Ltac2/tac2tactics.mli
index f63f7e722a..47a3fd5987 100644
--- a/user-contrib/Ltac2/tac2tactics.mli
+++ b/user-contrib/Ltac2/tac2tactics.mli
@@ -119,6 +119,8 @@ val eauto : Hints.debug -> int option -> int option -> constr thunk list ->
 val typeclasses_eauto : Class_tactics.search_strategy option -> int option ->
   Id.t list option -> unit Proofview.tactic
 
+val unify : constr -> constr -> unit tactic
+
 val inversion : Inv.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
 
 val contradiction : constr_with_bindings option -> unit tactic