5 files changed, 33 insertions, 12 deletions
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 457b8e1acf..4758ecf5bd 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1754,6 +1754,16 @@ let () = add_scope "constr" (fun arg ->
     Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act)
   )
 
+let () = add_scope "open_constr" (fun arg ->
+    let delimiters = List.map (function
+        | SexprRec (_, { v = Some s }, []) -> s
+        | _ -> scope_fail "open_constr" arg)
+        arg
+    in
+    let act e = Tac2quote.of_open_constr ~delimiters e in
+    Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act)
+  )
+
 let add_expr_scope name entry f =
   add_scope name begin function
   | [] -> Tac2entries.ScopeRule (Pcoq.Symbol.nterm entry, f)
@@ -1782,7 +1792,6 @@ let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_
 let () = add_expr_scope "goal_matching" q_goal_matching Tac2quote.of_goal_matching
 let () = add_expr_scope "format" Pcoq.Prim.lstring Tac2quote.of_format
 
-let () = add_generic_scope "open_constr" Pcoq.Constr.constr Tac2quote.wit_open_constr
 let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern
 
 (** seq scope, a bit hairy *)
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 6be5ba80d5..7af530ab0f 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -50,6 +50,12 @@ let q_pose = Pcoq.Entry.create "q_pose"
 let q_assert = Pcoq.Entry.create "q_assert"
 end
 
+let () =
+  let entries = [
+    Pcoq.AnyEntry Pltac.ltac2_expr;
+  ] in
+  Pcoq.register_grammars_by_name "ltac2" entries
+
 (** Tactic definition *)
 
 type tacdef = {
diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index 90c8528203..206f4df19d 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -467,7 +467,9 @@ let polymorphic ((n, t) : type_scheme) : mix_type_scheme =
 
 let warn_not_unit =
   CWarnings.create ~name:"not-unit" ~category:"ltac"
-    (fun () -> strbrk "The following expression should have type unit.")
+    (fun (env, t) ->
+      strbrk "The following expression should have type unit but has type " ++
+      pr_glbtype env t ++ str ".")
 
 let warn_redundant_clause =
   CWarnings.create ~name:"redundant-clause" ~category:"ltac"
@@ -480,7 +482,7 @@ let check_elt_unit loc env t =
   | GTypRef (Tuple 0, []) -> true
   | GTypRef _ -> false
   in
-  if not maybe_unit then warn_not_unit ?loc ()
+  if not maybe_unit then warn_not_unit ?loc (env, t)
 
 let check_elt_empty loc env t = match kind env t with
 | GTypVar _ ->
@@ -504,7 +506,7 @@ let check_unit ?loc t =
   | GTypRef (Tuple 0, []) -> true
   | GTypRef _ -> false
   in
-  if not maybe_unit then warn_not_unit ?loc ()
+  if not maybe_unit then warn_not_unit ?loc (env, t)
 
 let check_redundant_clause = function
 | [] -> ()
diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml
index d1a72fcfd1..2d65f9ec3e 100644
--- a/user-contrib/Ltac2/tac2quote.ml
+++ b/user-contrib/Ltac2/tac2quote.ml
@@ -102,18 +102,22 @@ let of_anti f = function
 
 let of_ident {loc;v=id} = inj_wit ?loc wit_ident id
 
+let quote_constr ?delimiters c =
+  let loc = Constrexpr_ops.constr_loc c in
+  Option.cata
+    (List.fold_left (fun c d ->
+          CAst.make ?loc @@ Constrexpr.CDelimiters(Id.to_string d, c))
+        c)
+    c delimiters
+
 let of_constr ?delimiters c =
   let loc = Constrexpr_ops.constr_loc c in
-  let c = Option.cata
-      (List.fold_left (fun c d ->
-           CAst.make ?loc @@ Constrexpr.CDelimiters(Id.to_string d, c))
-          c)
-      c delimiters
-  in
+  let c = quote_constr ?delimiters c in
   inj_wit ?loc wit_constr c
 
-let of_open_constr c =
+let of_open_constr ?delimiters c =
   let loc = Constrexpr_ops.constr_loc c in
+  let c = quote_constr ?delimiters c in
   inj_wit ?loc wit_open_constr c
 
 let of_bool ?loc b =
diff --git a/user-contrib/Ltac2/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli
index fcd1339cd7..6e2f548319 100644
--- a/user-contrib/Ltac2/tac2quote.mli
+++ b/user-contrib/Ltac2/tac2quote.mli
@@ -36,7 +36,7 @@ val of_ident : Id.t CAst.t -> raw_tacexpr
 
 val of_constr : ?delimiters:Id.t list -> Constrexpr.constr_expr -> raw_tacexpr
 
-val of_open_constr : Constrexpr.constr_expr -> raw_tacexpr
+val of_open_constr : ?delimiters:Id.t list -> Constrexpr.constr_expr -> raw_tacexpr
 
 val of_list : ?loc:Loc.t -> ('a -> raw_tacexpr) -> 'a list -> raw_tacexpr