aboutsummaryrefslogtreecommitdiff
path: root/user-contrib/Ltac2
diff options
context:
space:
mode:
Diffstat (limited to 'user-contrib/Ltac2')
-rw-r--r--user-contrib/Ltac2/Bool.v5
-rw-r--r--user-contrib/Ltac2/Notations.v2
-rw-r--r--user-contrib/Ltac2/Std.v2
-rw-r--r--user-contrib/Ltac2/tac2core.ml11
-rw-r--r--user-contrib/Ltac2/tac2entries.ml24
-rw-r--r--user-contrib/Ltac2/tac2intern.ml8
-rw-r--r--user-contrib/Ltac2/tac2quote.ml18
-rw-r--r--user-contrib/Ltac2/tac2quote.mli2
-rw-r--r--user-contrib/Ltac2/tac2stdlib.ml4
-rw-r--r--user-contrib/Ltac2/tac2tactics.ml2
-rw-r--r--user-contrib/Ltac2/tac2tactics.mli2
11 files changed, 62 insertions, 18 deletions
diff --git a/user-contrib/Ltac2/Bool.v b/user-contrib/Ltac2/Bool.v
index 624097728e..b201574808 100644
--- a/user-contrib/Ltac2/Bool.v
+++ b/user-contrib/Ltac2/Bool.v
@@ -48,7 +48,7 @@ Ltac2 xor x y :=
end
end.
-Ltac2 eq x y :=
+Ltac2 equal x y :=
match x with
| true
=> match y with
@@ -61,3 +61,6 @@ Ltac2 eq x y :=
| false => true
end
end.
+
+#[deprecated(note="Use Bool.equal", since="8.14")]
+Ltac2 eq := equal.
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/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..6aa31e9c91 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 = {
@@ -669,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
@@ -748,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 90c8528203..0171ddfcf8 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 "This 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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 06:48:26 +0000