aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--_CoqProject1
-rw-r--r--src/dune10
-rw-r--r--src/g_ltac2.ml416
-rw-r--r--src/tac2core.ml64
-rw-r--r--src/tac2entries.ml64
-rw-r--r--src/tac2entries.mli42
-rw-r--r--src/tac2ffi.ml2
-rw-r--r--src/tac2intern.ml18
-rw-r--r--src/tac2match.ml2
-rw-r--r--src/tac2print.ml14
-rw-r--r--src/tac2quote.ml2
-rw-r--r--src/tac2tactics.ml3
-rw-r--r--theories/Constr.v7
-rw-r--r--theories/Env.v22
-rw-r--r--theories/Ltac2.v1
15 files changed, 182 insertions, 86 deletions
diff --git a/_CoqProject b/_CoqProject
index 5af42197ea..15e02a6484 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -44,5 +44,6 @@ theories/Constr.v
theories/Pattern.v
theories/Fresh.v
theories/Std.v
+theories/Env.v
theories/Notations.v
theories/Ltac2.v
diff --git a/src/dune b/src/dune
new file mode 100644
index 0000000000..b0140aa809
--- /dev/null
+++ b/src/dune
@@ -0,0 +1,10 @@
+(library
+ (name ltac2)
+ (public_name coq.plugins.ltac2)
+ (modules_without_implementation tac2expr tac2qexpr tac2types)
+ (libraries coq.plugins.firstorder))
+
+(rule
+ (targets g_ltac2.ml)
+ (deps (:pp-file g_ltac2.ml4) )
+ (action (run coqp5 -loc loc -impl %{pp-file} -o %{targets})))
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 16e7278235..82ab53298e 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -81,14 +81,14 @@ let test_dollar_ident =
end
let tac2expr = Tac2entries.Pltac.tac2expr
-let tac2type = Gram.entry_create "tactic:tac2type"
-let tac2def_val = Gram.entry_create "tactic:tac2def_val"
-let tac2def_typ = Gram.entry_create "tactic:tac2def_typ"
-let tac2def_ext = Gram.entry_create "tactic:tac2def_ext"
-let tac2def_syn = Gram.entry_create "tactic:tac2def_syn"
-let tac2def_mut = Gram.entry_create "tactic:tac2def_mut"
-let tac2def_run = Gram.entry_create "tactic:tac2def_run"
-let tac2mode = Gram.entry_create "vernac:ltac2_command"
+let tac2type = Entry.create "tactic:tac2type"
+let tac2def_val = Entry.create "tactic:tac2def_val"
+let tac2def_typ = Entry.create "tactic:tac2def_typ"
+let tac2def_ext = Entry.create "tactic:tac2def_ext"
+let tac2def_syn = Entry.create "tactic:tac2def_syn"
+let tac2def_mut = Entry.create "tactic:tac2def_mut"
+let tac2def_run = Entry.create "tactic:tac2def_run"
+let tac2mode = Entry.create "vernac:ltac2_command"
let ltac1_expr = Pltac.tactic_expr
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 13265ee080..8ee239f803 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -20,8 +20,8 @@ open Proofview.Notations
module Value = Tac2ffi
open Value
-let std_core n = KerName.make2 Tac2env.std_prefix (Label.of_id (Id.of_string_soft n))
-let coq_core n = KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
+let std_core n = KerName.make Tac2env.std_prefix (Label.of_id (Id.of_string_soft n))
+let coq_core n = KerName.make Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
module Core =
struct
@@ -494,6 +494,26 @@ let () = define3 "constr_closenl" (list ident) int constr begin fun ids k c ->
return (Value.of_constr ans)
end
+let () = define1 "constr_case" (repr_ext val_inductive) begin fun ind ->
+ Proofview.tclENV >>= fun env ->
+ try
+ let ans = Inductiveops.make_case_info env ind Constr.RegularStyle in
+ return (Value.of_ext Value.val_case ans)
+ with e when CErrors.noncritical e ->
+ throw err_notfound
+end
+
+let () = define2 "constr_constructor" (repr_ext val_inductive) int begin fun (ind, i) k ->
+ Proofview.tclENV >>= fun env ->
+ try
+ let open Declarations in
+ let ans = Environ.lookup_mind ind env in
+ let _ = ans.mind_packets.(i).mind_consnames.(k) in
+ return (Value.of_ext val_constructor ((ind, i), (k + 1)))
+ with e when CErrors.noncritical e ->
+ throw err_notfound
+end
+
let () = define3 "constr_in_context" ident constr closure begin fun id t c ->
Proofview.Goal.goals >>= function
| [gl] ->
@@ -801,6 +821,42 @@ let () = define2 "fresh_fresh" (repr_ext val_free) ident begin fun avoid id ->
return (Value.of_ident nid)
end
+(** Env *)
+
+let () = define1 "env_get" (list ident) begin fun ids ->
+ let r = match ids with
+ | [] -> None
+ | _ :: _ as ids ->
+ let (id, path) = List.sep_last ids in
+ let path = DirPath.make (List.rev path) in
+ let fp = Libnames.make_path path id in
+ try Some (Nametab.global_of_path fp) with Not_found -> None
+ in
+ return (Value.of_option Value.of_reference r)
+end
+
+let () = define1 "env_expand" (list ident) begin fun ids ->
+ let r = match ids with
+ | [] -> []
+ | _ :: _ as ids ->
+ let (id, path) = List.sep_last ids in
+ let path = DirPath.make (List.rev path) in
+ let qid = Libnames.make_qualid path id in
+ Nametab.locate_all qid
+ in
+ return (Value.of_list Value.of_reference r)
+end
+
+let () = define1 "env_path" reference begin fun r ->
+ match Nametab.path_of_global r with
+ | fp ->
+ let (path, id) = Libnames.repr_path fp in
+ let path = DirPath.repr path in
+ return (Value.of_list Value.of_ident (List.rev_append path [id]))
+ | exception Not_found ->
+ throw err_notfound
+end
+
(** ML types *)
let constr_flags () =
@@ -974,7 +1030,7 @@ let () =
let c, sigma = Pfedit.refine_by_tactic env sigma concl tac in
(EConstr.of_constr c, sigma)
in
- Pretyping.register_constr_interp0 wit_ltac2 interp
+ GlobEnv.register_constr_interp0 wit_ltac2 interp
let () =
let interp ist env sigma concl id =
@@ -984,7 +1040,7 @@ let () =
let sigma = Typing.check env sigma c concl in
(c, sigma)
in
- Pretyping.register_constr_interp0 wit_ltac2_quotation interp
+ GlobEnv.register_constr_interp0 wit_ltac2_quotation interp
let () =
let pr_raw id = Genprint.PrinterBasic mt in
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 8ebfeec948..bba4680a72 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -22,28 +22,28 @@ open Tac2intern
module Pltac =
struct
-let tac2expr = Pcoq.Gram.entry_create "tactic:tac2expr"
-
-let q_ident = Pcoq.Gram.entry_create "tactic:q_ident"
-let q_bindings = Pcoq.Gram.entry_create "tactic:q_bindings"
-let q_with_bindings = Pcoq.Gram.entry_create "tactic:q_with_bindings"
-let q_intropattern = Pcoq.Gram.entry_create "tactic:q_intropattern"
-let q_intropatterns = Pcoq.Gram.entry_create "tactic:q_intropatterns"
-let q_destruction_arg = Pcoq.Gram.entry_create "tactic:q_destruction_arg"
-let q_induction_clause = Pcoq.Gram.entry_create "tactic:q_induction_clause"
-let q_conversion = Pcoq.Gram.entry_create "tactic:q_conversion"
-let q_rewriting = Pcoq.Gram.entry_create "tactic:q_rewriting"
-let q_clause = Pcoq.Gram.entry_create "tactic:q_clause"
-let q_dispatch = Pcoq.Gram.entry_create "tactic:q_dispatch"
-let q_occurrences = Pcoq.Gram.entry_create "tactic:q_occurrences"
-let q_reference = Pcoq.Gram.entry_create "tactic:q_reference"
-let q_strategy_flag = Pcoq.Gram.entry_create "tactic:q_strategy_flag"
-let q_constr_matching = Pcoq.Gram.entry_create "tactic:q_constr_matching"
-let q_goal_matching = Pcoq.Gram.entry_create "tactic:q_goal_matching"
-let q_hintdb = Pcoq.Gram.entry_create "tactic:q_hintdb"
-let q_move_location = Pcoq.Gram.entry_create "tactic:q_move_location"
-let q_pose = Pcoq.Gram.entry_create "tactic:q_pose"
-let q_assert = Pcoq.Gram.entry_create "tactic:q_assert"
+let tac2expr = Pcoq.Entry.create "tactic:tac2expr"
+
+let q_ident = Pcoq.Entry.create "tactic:q_ident"
+let q_bindings = Pcoq.Entry.create "tactic:q_bindings"
+let q_with_bindings = Pcoq.Entry.create "tactic:q_with_bindings"
+let q_intropattern = Pcoq.Entry.create "tactic:q_intropattern"
+let q_intropatterns = Pcoq.Entry.create "tactic:q_intropatterns"
+let q_destruction_arg = Pcoq.Entry.create "tactic:q_destruction_arg"
+let q_induction_clause = Pcoq.Entry.create "tactic:q_induction_clause"
+let q_conversion = Pcoq.Entry.create "tactic:q_conversion"
+let q_rewriting = Pcoq.Entry.create "tactic:q_rewriting"
+let q_clause = Pcoq.Entry.create "tactic:q_clause"
+let q_dispatch = Pcoq.Entry.create "tactic:q_dispatch"
+let q_occurrences = Pcoq.Entry.create "tactic:q_occurrences"
+let q_reference = Pcoq.Entry.create "tactic:q_reference"
+let q_strategy_flag = Pcoq.Entry.create "tactic:q_strategy_flag"
+let q_constr_matching = Pcoq.Entry.create "tactic:q_constr_matching"
+let q_goal_matching = Pcoq.Entry.create "tactic:q_goal_matching"
+let q_hintdb = Pcoq.Entry.create "tactic:q_hintdb"
+let q_move_location = Pcoq.Entry.create "tactic:q_move_location"
+let q_pose = Pcoq.Entry.create "tactic:q_pose"
+let q_assert = Pcoq.Entry.create "tactic:q_assert"
end
(** Tactic definition *)
@@ -100,8 +100,8 @@ type typdef = {
}
let change_kn_label kn id =
- let (mp, dp, _) = KerName.repr kn in
- KerName.make mp dp (Label.of_id id)
+ let mp = KerName.modpath kn in
+ KerName.make mp (Label.of_id id)
let change_sp_label sp id =
let (dp, _) = Libnames.repr_path sp in
@@ -750,14 +750,14 @@ let perform_eval e =
Proof_global.give_me_the_proof ()
with Proof_global.NoCurrentProof ->
let sigma = Evd.from_env env in
- Vernacexpr.SelectAll, Proof.start sigma []
+ Goal_select.SelectAll, Proof.start sigma []
in
let v = match selector with
- | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i v
- | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l v
- | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id v
- | Vernacexpr.SelectAll -> v
- | Vernacexpr.SelectAlreadyFocused -> assert false (** TODO **)
+ | Goal_select.SelectNth i -> Proofview.tclFOCUS i i v
+ | Goal_select.SelectList l -> Proofview.tclFOCUSLIST l v
+ | Goal_select.SelectId id -> Proofview.tclFOCUSID id v
+ | Goal_select.SelectAll -> v
+ | Goal_select.SelectAlreadyFocused -> assert false (** TODO **)
in
(** HACK: the API doesn't allow to return a value *)
let ans = ref None in
@@ -805,7 +805,7 @@ let pr_frame = function
let () = register_handler begin function
| Tac2interp.LtacError (kn, args) ->
- let t_exn = KerName.make2 Tac2env.coq_prefix (Label.make "exn") in
+ let t_exn = KerName.make Tac2env.coq_prefix (Label.make "exn") in
let v = Tac2ffi.of_open (kn, args) in
let t = GTypRef (Other t_exn, []) in
let c = Tac2print.pr_valexpr (Global.env ()) Evd.empty v t in
@@ -897,7 +897,7 @@ let register_prim_alg name params def =
let def = { typdef_local = false; typdef_expr = def } in
ignore (Lib.add_leaf id (inTypDef def))
-let coq_def n = KerName.make2 Tac2env.coq_prefix (Label.make n)
+let coq_def n = KerName.make Tac2env.coq_prefix (Label.make n)
let def_unit = {
typdef_local = false;
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 37944981d7..f97e35fec0 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -56,32 +56,32 @@ val backtrace : backtrace Exninfo.t
module Pltac :
sig
-val tac2expr : raw_tacexpr Pcoq.Gram.entry
+val tac2expr : raw_tacexpr Pcoq.Entry.t
(** Quoted entries. To be used for complex notations. *)
open Tac2qexpr
-val q_ident : Id.t CAst.t or_anti Pcoq.Gram.entry
-val q_bindings : bindings Pcoq.Gram.entry
-val q_with_bindings : bindings Pcoq.Gram.entry
-val q_intropattern : intro_pattern Pcoq.Gram.entry
-val q_intropatterns : intro_pattern list CAst.t Pcoq.Gram.entry
-val q_destruction_arg : destruction_arg Pcoq.Gram.entry
-val q_induction_clause : induction_clause Pcoq.Gram.entry
-val q_conversion : conversion Pcoq.Gram.entry
-val q_rewriting : rewriting Pcoq.Gram.entry
-val q_clause : clause Pcoq.Gram.entry
-val q_dispatch : dispatch Pcoq.Gram.entry
-val q_occurrences : occurrences Pcoq.Gram.entry
-val q_reference : reference or_anti Pcoq.Gram.entry
-val q_strategy_flag : strategy_flag Pcoq.Gram.entry
-val q_constr_matching : constr_matching Pcoq.Gram.entry
-val q_goal_matching : goal_matching Pcoq.Gram.entry
-val q_hintdb : hintdb Pcoq.Gram.entry
-val q_move_location : move_location Pcoq.Gram.entry
-val q_pose : pose Pcoq.Gram.entry
-val q_assert : assertion Pcoq.Gram.entry
+val q_ident : Id.t CAst.t or_anti Pcoq.Entry.t
+val q_bindings : bindings Pcoq.Entry.t
+val q_with_bindings : bindings Pcoq.Entry.t
+val q_intropattern : intro_pattern Pcoq.Entry.t
+val q_intropatterns : intro_pattern list CAst.t Pcoq.Entry.t
+val q_destruction_arg : destruction_arg Pcoq.Entry.t
+val q_induction_clause : induction_clause Pcoq.Entry.t
+val q_conversion : conversion Pcoq.Entry.t
+val q_rewriting : rewriting Pcoq.Entry.t
+val q_clause : clause Pcoq.Entry.t
+val q_dispatch : dispatch Pcoq.Entry.t
+val q_occurrences : occurrences Pcoq.Entry.t
+val q_reference : reference or_anti Pcoq.Entry.t
+val q_strategy_flag : strategy_flag Pcoq.Entry.t
+val q_constr_matching : constr_matching Pcoq.Entry.t
+val q_goal_matching : goal_matching Pcoq.Entry.t
+val q_hintdb : hintdb Pcoq.Entry.t
+val q_move_location : move_location Pcoq.Entry.t
+val q_pose : pose Pcoq.Entry.t
+val q_assert : assertion Pcoq.Entry.t
end
(** {5 Hooks} *)
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index a719970a57..df1857c3e7 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -229,7 +229,7 @@ let internal_err =
let coq_prefix =
MPfile (DirPath.make (List.map Id.of_string ["Init"; "Ltac2"]))
in
- KerName.make2 coq_prefix (Label.of_id (Id.of_string "Internal"))
+ KerName.make coq_prefix (Label.of_id (Id.of_string "Internal"))
(** FIXME: handle backtrace in Ltac2 exceptions *)
let of_exn c = match fst c with
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index f3b222df21..fe615853ce 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -19,7 +19,7 @@ open Tac2expr
(** Hardwired types and constants *)
-let coq_type n = KerName.make2 Tac2env.coq_prefix (Label.make n)
+let coq_type n = KerName.make Tac2env.coq_prefix (Label.make n)
let t_int = coq_type "int"
let t_string = coq_type "string"
@@ -356,8 +356,8 @@ let rec unify0 env t1 t2 = match kind env t1, kind env t2 with
let unify ?loc env t1 t2 =
try unify0 env t1 t2
with CannotUnify (u1, u2) ->
- user_err ?loc (str "This expression has type " ++ pr_glbtype env t1 ++
- str " but an expression was expected of type " ++ pr_glbtype env t2)
+ user_err ?loc (str "This expression has type" ++ spc () ++ pr_glbtype env t1 ++
+ spc () ++ str "but an expression was expected of type" ++ spc () ++ pr_glbtype env t2)
let unify_arrow ?loc env ft args =
let ft0 = ft in
@@ -372,11 +372,11 @@ let unify_arrow ?loc env ft args =
iter ft args true
| GTypRef _, _ :: _ ->
if is_fun then
- user_err ?loc (str "This function has type " ++ pr_glbtype env ft0 ++
- str " and is applied to too many arguments")
+ user_err ?loc (str "This function has type" ++ spc () ++ pr_glbtype env ft0 ++
+ spc () ++ str "and is applied to too many arguments")
else
- user_err ?loc (str "This expression has type " ++ pr_glbtype env ft0 ++
- str " and is not a function")
+ user_err ?loc (str "This expression has type" ++ spc () ++ pr_glbtype env ft0 ++
+ spc () ++ str "and is not a function")
in
iter ft args false
@@ -475,13 +475,13 @@ let check_elt_empty loc env t = match kind env t with
| GTypVar _ ->
user_err ?loc (str "Cannot infer an empty type for this expression")
| GTypArrow _ | GTypRef (Tuple _, _) ->
- user_err ?loc (str "Type " ++ pr_glbtype env t ++ str " is not an empty type")
+ user_err ?loc (str "Type" ++ spc () ++ pr_glbtype env t ++ spc () ++ str "is not an empty type")
| GTypRef (Other kn, _) ->
let def = Tac2env.interp_type kn in
match def with
| _, GTydAlg { galg_constructors = [] } -> kn
| _ ->
- user_err ?loc (str "Type " ++ pr_glbtype env t ++ str " is not an empty type")
+ user_err ?loc (str "Type" ++ spc () ++ pr_glbtype env t ++ spc () ++ str "is not an empty type")
let check_unit ?loc t =
let env = empty_env () in
diff --git a/src/tac2match.ml b/src/tac2match.ml
index a3140eabea..c9e549d47e 100644
--- a/src/tac2match.ml
+++ b/src/tac2match.ml
@@ -181,7 +181,7 @@ module PatternMatching (E:StaticEnvironment) = struct
pattern_match_term pat (NamedDecl.get_type decl) >>= fun ctx ->
return (id, ctx)
- let hyp_match_body_and_type bodypat typepat hyps =
+ let _hyp_match_body_and_type bodypat typepat hyps =
pick hyps >>= function
| LocalDef (id,body,hyp) ->
pattern_match_term bodypat body >>= fun ctx_body ->
diff --git a/src/tac2print.ml b/src/tac2print.ml
index cab1530d15..0b20cf9f58 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -16,13 +16,13 @@ open Tac2ffi
(** Utils *)
let change_kn_label kn id =
- let (mp, dp, _) = KerName.repr kn in
- KerName.make mp dp (Label.of_id id)
+ let mp = KerName.modpath kn in
+ KerName.make mp (Label.of_id id)
let paren p = hov 2 (str "(" ++ p ++ str ")")
let t_list =
- KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string "list"))
+ KerName.make Tac2env.coq_prefix (Label.of_id (Id.of_string "list"))
(** Type printing *)
@@ -35,7 +35,7 @@ type typ_level =
| T0
let t_unit =
- KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string "unit"))
+ KerName.make Tac2env.coq_prefix (Label.of_id (Id.of_string "unit"))
let pr_typref kn =
Libnames.pr_qualid (Tac2env.shortest_qualid_of_type kn)
@@ -49,7 +49,7 @@ let pr_glbtype_gen pr lvl c =
| T5_r | T5_l | T2 | T1 -> fun x -> x
| T0 -> paren
in
- paren (pr_glbtype lvl t ++ spc () ++ pr_typref kn)
+ paren (pr_glbtype T1 t ++ spc () ++ pr_typref kn)
| GTypRef (Other kn, tl) ->
let paren = match lvl with
| T5_r | T5_l | T2 | T1 -> fun x -> x
@@ -435,7 +435,7 @@ and pr_val_list env sigma args tpe =
str "[" ++ prlist_with_sep pr_semicolon pr args ++ str "]"
let register_init n f =
- let kn = KerName.make2 Tac2env.coq_prefix (Label.make n) in
+ let kn = KerName.make Tac2env.coq_prefix (Label.make n) in
register_val_printer kn { val_printer = fun env sigma v _ -> f env sigma v }
let () = register_init "int" begin fun _ _ n ->
@@ -476,7 +476,7 @@ let () = register_init "err" begin fun _ _ e ->
end
let () =
- let kn = KerName.make2 Tac2env.coq_prefix (Label.make "array") in
+ let kn = KerName.make Tac2env.coq_prefix (Label.make "array") in
let val_printer env sigma v arg = match arg with
| [arg] ->
let (_, v) = to_block v in
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 1d742afd83..3bddfe7594 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -32,7 +32,7 @@ let control_prefix = prefix_gen "Control"
let pattern_prefix = prefix_gen "Pattern"
let array_prefix = prefix_gen "Array"
-let kername prefix n = KerName.make2 prefix (Label.of_id (Id.of_string_soft n))
+let kername prefix n = KerName.make prefix (Label.of_id (Id.of_string_soft n))
let std_core n = kername Tac2env.std_prefix n
let coq_core n = kername Tac2env.coq_prefix n
let control_core n = kername control_prefix n
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 3c464469f0..25431af2ea 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -159,8 +159,7 @@ let specialize c pat =
let change pat c cl =
let open Tac2ffi in
Proofview.Goal.enter begin fun gl ->
- let env = Proofview.Goal.env gl in
- let c subst sigma =
+ let c subst env sigma =
let subst = Array.map_of_list snd (Id.Map.bindings subst) in
delayed_of_tactic (Tac2ffi.app_fun1 c (array constr) constr subst) env sigma
in
diff --git a/theories/Constr.v b/theories/Constr.v
index 072c613920..d8d222730e 100644
--- a/theories/Constr.v
+++ b/theories/Constr.v
@@ -57,6 +57,13 @@ Ltac2 @ external closenl : ident list -> int -> constr -> constr := "ltac2" "con
(** [closenl [x₁;...;xₙ] k c] abstracts over variables [x₁;...;xₙ] and replaces them with
[Rel(k); ...; Rel(k+n-1)] in [c]. If two names are identical, the one of least index is kept. *)
+Ltac2 @ external case : inductive -> case := "ltac2" "constr_case".
+(** Generate the case information for a given inductive type. *)
+
+Ltac2 @ external constructor : inductive -> int -> constructor := "ltac2" "constr_constructor".
+(** Generate the i-th constructor for a given inductive type. Indexing starts
+ at 0. Panics if there is no such constructor. *)
+
End Unsafe.
Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "ltac2" "constr_in_context".
diff --git a/theories/Env.v b/theories/Env.v
new file mode 100644
index 0000000000..7e36aa7990
--- /dev/null
+++ b/theories/Env.v
@@ -0,0 +1,22 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+Require Import Std.
+
+Ltac2 @ external get : ident list -> Std.reference option := "ltac2" "env_get".
+(** Returns the global reference corresponding to the absolute name given as
+ argument if it exists. *)
+
+Ltac2 @ external expand : ident list -> Std.reference list := "ltac2" "env_expand".
+(** Returns the list of all global references whose absolute name contains
+ the argument list as a prefix. *)
+
+Ltac2 @ external path : Std.reference -> ident list := "ltac2" "env_path".
+(** Returns the absolute name of the given reference. Panics if the reference
+ does not exist. *)
diff --git a/theories/Ltac2.v b/theories/Ltac2.v
index 7b2f592ac6..3fe71f4c65 100644
--- a/theories/Ltac2.v
+++ b/theories/Ltac2.v
@@ -18,4 +18,5 @@ Require Ltac2.Control.
Require Ltac2.Fresh.
Require Ltac2.Pattern.
Require Ltac2.Std.
+Require Ltac2.Env.
Require Export Ltac2.Notations.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 11:55:04 +0000