aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/coretactics.ml432
-rw-r--r--plugins/ltac/evar_tactics.ml15
-rw-r--r--plugins/ltac/extraargs.ml42
-rw-r--r--plugins/ltac/extratactics.ml47
-rw-r--r--plugins/ltac/g_tactic.ml46
-rw-r--r--plugins/ltac/pptactic.ml8
-rw-r--r--plugins/ltac/rewrite.ml40
-rw-r--r--plugins/ltac/tacentries.ml12
-rw-r--r--plugins/ltac/tacintern.ml2
9 files changed, 75 insertions, 49 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 6890b31981..0a13a20a97 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -326,3 +326,35 @@ let initial_atomic () =
]
let () = Mltop.declare_cache_obj initial_atomic "coretactics"
+
+(* First-class Ltac access to primitive blocks *)
+
+let initial_name s = { mltac_plugin = "coretactics"; mltac_tactic = s; }
+let initial_entry s = { mltac_name = initial_name s; mltac_index = 0; }
+
+let register_list_tactical name f =
+ let tac args ist = match args with
+ | [v] ->
+ begin match Tacinterp.Value.to_list v with
+ | None -> Tacticals.New.tclZEROMSG (Pp.str "Expected a list")
+ | Some tacs ->
+ let tacs = List.map (fun tac -> Tacinterp.tactic_of_value ist tac) tacs in
+ f tacs
+ end
+ | _ -> assert false
+ in
+ Tacenv.register_ml_tactic (initial_name name) [|tac|]
+
+let () = register_list_tactical "first" Tacticals.New.tclFIRST
+let () = register_list_tactical "solve" Tacticals.New.tclSOLVE
+
+let initial_tacticals () =
+ let idn n = Id.of_string (Printf.sprintf "_%i" n) in
+ let varn n = Reference (ArgVar (None, idn n)) in
+ let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in
+ List.iter iter [
+ "first", TacFun ([Name (idn 0)], TacML (None, (initial_entry "first", [varn 0])));
+ "solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0])));
+ ]
+
+let () = Mltop.declare_cache_obj initial_tacticals "coretactics"
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 470a93f2bc..bf84f61a5b 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -56,17 +56,16 @@ let instantiate_tac n c ido =
InHyp ->
(match decl with
| LocalAssum (_,typ) -> evar_list sigma (EConstr.of_constr typ)
- | _ -> error
- "Please be more specific: in type or value?")
+ | _ -> user_err Pp.(str "Please be more specific: in type or value?"))
| InHypTypeOnly ->
evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl))
| InHypValueOnly ->
(match decl with
| LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body)
- | _ -> error "Not a defined hypothesis.") in
+ | _ -> user_err Pp.(str "Not a defined hypothesis.")) in
if List.length evl < n then
- error "Not enough uninstantiated existential variables.";
- if n <= 0 then error "Incorrect existential variable index.";
+ user_err Pp.(str "Not enough uninstantiated existential variables.");
+ if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
let evk,_ = List.nth evl (n-1) in
instantiate_evar evk c sigma gl
end
@@ -76,7 +75,7 @@ let instantiate_tac_by_name id c =
let sigma = gl.sigma in
let evk =
try Evd.evar_key id sigma
- with Not_found -> error "Unknown existential variable." in
+ with Not_found -> user_err Pp.(str "Unknown existential variable.") in
instantiate_evar evk c sigma gl
end
@@ -109,8 +108,8 @@ let hget_evar n =
let concl = Proofview.Goal.concl gl in
let evl = evar_list sigma concl in
if List.length evl < n then
- error "Not enough uninstantiated existential variables.";
- if n <= 0 then error "Incorrect existential variable index.";
+ user_err Pp.(str "Not enough uninstantiated existential variables.");
+ if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
let ev = List.nth evl (n-1) in
let ev_type = EConstr.existential_type sigma ev in
Tactics.change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl))
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index a3310c2d8c..fdb8d34618 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -90,7 +90,7 @@ let occurrences_of = function
| n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl)
| nl ->
if List.exists (fun n -> n < 0) nl then
- CErrors.error "Illegal negative occurrence number.";
+ CErrors.user_err Pp.(str "Illegal negative occurrence number.");
OnlyOccurrences nl
let coerce_to_int v = match Value.to_int v with
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index cbd8a7f0fe..d68139a4b4 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -306,7 +306,7 @@ let project_hint pri l2r r =
| _ -> assert false in
let p =
if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
- let p = EConstr.of_constr p in
+ let p = EConstr.of_constr @@ Universes.constr_of_global p in
let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
let c = it_mkLambda_or_LetIn
(mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
@@ -735,7 +735,8 @@ let rewrite_except h =
let refl_equal =
let coq_base_constant s =
- Coqlib.gen_constant_in_modules "RecursiveDefinition"
+ Universes.constr_of_global @@
+ Coqlib.gen_reference_in_modules "RecursiveDefinition"
(Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s in
function () -> (coq_base_constant "eq_refl")
@@ -1084,7 +1085,7 @@ let decompose l c =
let sigma = Tacmach.New.project gl in
let to_ind c =
if isInd sigma c then fst (destInd sigma c)
- else error "not an inductive type"
+ else user_err Pp.(str "not an inductive type")
in
let l = List.map to_ind l in
Elim.h_decompose l c
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 257100b012..1404b1c1f1 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -117,8 +117,8 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
| _, Some x ->
let ids = List.map snd (List.flatten (List.map pi1 bl)) in
(try List.index Names.Name.equal (snd x) ids
- with Not_found -> error "No such fix variable.")
- | _ -> error "Cannot guess decreasing argument of fix." in
+ with Not_found -> user_err Pp.(str "No such fix variable."))
+ | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in
(id,n, CAst.make ~loc @@ CProdN(bl,ty))
let mk_cofix_tac (loc,id,bl,ann,ty) =
@@ -152,7 +152,7 @@ let mkTacCase with_evar = function
| ic ->
if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
then
- error "Use of numbers as direct arguments of 'case' is not supported.";
+ user_err Pp.(str "Use of numbers as direct arguments of 'case' is not supported.");
TacInductionDestruct (false,with_evar,ic)
let rec mkCLambdaN_simple_loc ?loc bll c =
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 75ab1c5ee6..a001c6a2ba 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -348,7 +348,7 @@ type 'a extra_genarg_printer =
let bll = List.map (fun (x, _, y) -> x, y) bll in
if nb >= n then (List.rev (bll@acc)), a
else strip_ty (bll@acc) (n-nb) a
- | _ -> error "Cannot translate fix tactic: not enough products" in
+ | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
let pr_ltac_or_var pr = function
@@ -1089,7 +1089,7 @@ type 'a extra_genarg_printer =
match ty.CAst.v with
Glob_term.GProd(na,Explicit,a,b) ->
strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b
- | _ -> error "Cannot translate fix tactic: not enough products" in
+ | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
let raw_printers =
@@ -1160,7 +1160,7 @@ type 'a extra_genarg_printer =
match Term.kind_of_term ty with
Term.Prod(na,a,b) ->
strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
- | _ -> error "Cannot translate fix tactic: not enough products" in
+ | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
let pr_atomic_tactic_level env sigma n t =
@@ -1210,7 +1210,7 @@ let declare_extra_genarg_pprule wit
(h : 'c extra_genarg_printer) =
begin match wit with
| ExtraArg s -> ()
- | _ -> error "Can declare a pretty-printing rule only for extra argument types."
+ | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.")
end;
let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in
let g x =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index e8c9f4ebaa..966b11d0e7 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -55,22 +55,16 @@ let init_setoid () =
if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
+let lazy_find_reference dir s =
+ let gr = lazy (Coqlib.coq_reference "generalized rewriting" dir s) in
+ fun () -> Lazy.force gr
-let try_find_global_reference dir s =
- let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in
- try Nametab.global_of_path sp
- with Not_found ->
- anomaly (str "Global reference " ++ str s ++ str " not found in generalized rewriting")
-
-let find_reference dir s =
- let gr = lazy (try_find_global_reference dir s) in
- fun () -> Lazy.force gr
+let find_reference dir s = Coqlib.coq_reference "generalized rewriting" dir s
type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
let find_global dir s =
- let gr = lazy (try_find_global_reference dir s) in
+ let gr = lazy (find_reference dir s) in
fun (evd,cstrs) ->
let sigma = Sigma.Unsafe.of_evar_map evd in
let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in
@@ -81,7 +75,7 @@ let find_global dir s =
(** Global constants. *)
-let coq_eq_ref = find_reference ["Init"; "Logic"] "eq"
+let coq_eq_ref = lazy_find_reference ["Init"; "Logic"] "eq"
let coq_eq = find_global ["Init"; "Logic"] "eq"
let coq_f_equal = find_global ["Init"; "Logic"] "f_equal"
let coq_all = find_global ["Init"; "Logic"] "all"
@@ -158,11 +152,11 @@ end) = struct
let forall_relation = find_global morphisms "forall_relation"
let pointwise_relation = find_global morphisms "pointwise_relation"
- let forall_relation_ref = find_reference morphisms "forall_relation"
- let pointwise_relation_ref = find_reference morphisms "pointwise_relation"
+ let forall_relation_ref = lazy_find_reference morphisms "forall_relation"
+ let pointwise_relation_ref = lazy_find_reference morphisms "pointwise_relation"
let respectful = find_global morphisms "respectful"
- let respectful_ref = find_reference morphisms "respectful"
+ let respectful_ref = lazy_find_reference morphisms "respectful"
let default_relation = find_global ["Classes"; "SetoidTactics"] "DefaultRelation"
@@ -174,8 +168,8 @@ end) = struct
let rewrite_relation_class = find_global relation_classes "RewriteRelation"
- let proper_class = lazy (class_info (try_find_global_reference morphisms "Proper"))
- let proper_proxy_class = lazy (class_info (try_find_global_reference morphisms "ProperProxy"))
+ let proper_class = lazy (class_info (find_reference morphisms "Proper"))
+ let proper_proxy_class = lazy (class_info (find_reference morphisms "ProperProxy"))
let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
@@ -241,7 +235,7 @@ end) = struct
let liftarg = mkLambda (na, ty, arg) in
let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in
if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
- else error "build_signature: no constraint can apply on a dependent argument"
+ else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument")
| _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products")
| _, [] ->
(match finalcstr with
@@ -478,7 +472,7 @@ type hypinfo = {
let get_symmetric_proof b =
if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof
-let error_no_relation () = error "Cannot find a relation to rewrite."
+let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.")
let rec decompose_app_rel env evd t =
(** Head normalize for compatibility with the old meta mechanism *)
@@ -531,7 +525,7 @@ let decompose_applied_relation env sigma (c,l) =
let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *)
match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with
| Some c -> c
- | None -> error "Cannot find an homogeneous relation to rewrite."
+ | None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.")
let rewrite_db = "rewrite"
@@ -837,7 +831,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
sigargs, r.rew_to :: typeargs')
| None ->
if not (Option.is_empty y) then
- error "Cannot rewrite inside dependent arguments of a function";
+ user_err Pp.(str "Cannot rewrite inside dependent arguments of a function");
x :: acc, x :: subst, evars, sigargs, x :: typeargs')
([], [], evars, sigargs, []) args args'
in
@@ -1425,7 +1419,7 @@ module Strategies =
let unfolded =
try Tacred.try_red_product env sigma c
with e when CErrors.noncritical e ->
- error "fold: the term is not unfoldable !"
+ user_err Pp.(str "fold: the term is not unfoldable !")
in
try
let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in
@@ -2204,7 +2198,7 @@ let setoid_symmetry_in id =
let rec split_last_two = function
| [c1;c2] -> [],(c1, c2)
| x::y::z -> let l,res = split_last_two (y::z) in x::l, res
- | _ -> error "Cannot find an equivalence relation to rewrite."
+ | _ -> user_err Pp.(str "Cannot find an equivalence relation to rewrite.")
in
let others,(c1,c2) = split_last_two args in
let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4d7b0f9296..75f89a81e1 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -60,7 +60,7 @@ let get_tacentry n m =
else EntryName (rawwit Tacarg.wit_tactic, atactic n)
let get_separator = function
-| None -> error "Missing separator."
+| None -> user_err Pp.(str "Missing separator.")
| Some sep -> sep
let rec parse_user_entry s sep =
@@ -110,7 +110,7 @@ let get_tactic_entry n =
else if 1<=n && n<5 then
Pltac.tactic_expr, Some (Extend.Level (string_of_int n))
else
- error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
+ user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^"."))
(**********************************************************************)
(** State of the grammar extensions *)
@@ -170,7 +170,7 @@ let add_tactic_entry (kn, ml, tg) state =
in
let () =
if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
- error "Notation for simple tactic must start with an identifier."
+ user_err Pp.(str "Notation for simple tactic must start with an identifier.")
in
let map = function
| TacTerm s -> GramTerminal s
@@ -208,7 +208,7 @@ let interp_prod_item = function
| None ->
if String.Map.mem s !entry_names then String.Map.find s !entry_names
else begin match ArgT.name s with
- | None -> error ("Unknown entry "^s^".")
+ | None -> user_err Pp.(str ("Unknown entry "^s^"."))
| Some arg -> arg
end
| Some n ->
@@ -253,8 +253,8 @@ let pprule pa = {
let check_key key =
if Tacenv.check_alias key then
- error "Conflicting tactic notations keys. This can happen when including \
- twice the same module."
+ user_err Pp.(str "Conflicting tactic notations keys. This can happen when including \
+ twice the same module.")
let cache_tactic_notation (_, tobj) =
let key = tobj.tacobj_key in
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 6c7eb8c899..e431a13bc2 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -252,7 +252,7 @@ and intern_or_and_intro_pattern lf ist = function
let intern_or_and_intro_pattern_loc lf ist = function
| ArgVar (_,id) as x ->
if find_var id ist then x
- else error "Disjunctive/conjunctive introduction pattern expected."
+ else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.")
| ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l)
let intern_intro_pattern_naming_loc lf ist (loc,pat) =
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 01:59:48 +0000