aboutsummaryrefslogtreecommitdiff
path: root/plugins/decl_mode
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/decl_mode')
-rw-r--r--plugins/decl_mode/decl_interp.ml16
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml20
-rw-r--r--plugins/decl_mode/g_decl_mode.ml43
-rw-r--r--plugins/decl_mode/ppdecl_proof.ml1
4 files changed, 21 insertions, 19 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index a862423e99..3b233d6ef4 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Ltac_plugin
open CErrors
open Util
open Names
@@ -90,8 +91,8 @@ let rec add_vars_of_simple_pattern globs = function
(* Loc.raise loc
(UserError ("simple_pattern",str "\"as\" is not allowed here"))*)
| CPatOr (loc, _)->
- Loc.raise loc
- (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here"))
+ Loc.raise ~loc
+ (UserError (Some "simple_pattern",str "\"(_ | _)\" is not allowed here"))
| CPatDelimiters (_,_,p) ->
add_vars_of_simple_pattern globs p
| CPatCstr (_,_,pl1,pl2) ->
@@ -263,7 +264,7 @@ let prod_one_id (loc,id) glob =
GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob)
let let_in_one_alias (id,pat) glob =
- GLetIn (Loc.ghost,Name id, glob_of_pat pat, glob)
+ GLetIn (Loc.ghost,Name id, glob_of_pat pat, None, glob)
let rec bind_primary_aliases map pat =
match pat with
@@ -328,7 +329,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
let _ =
let expected = mib.Declarations.mind_nparams - num_params in
if not (Int.equal (List.length params) expected) then
- errorlabstrm "suppose it is"
+ user_err ~hdr:"suppose it is"
(str "Wrong number of extra arguments: " ++
(if Int.equal expected 0 then str "none" else int expected) ++ spc () ++
str "expected.") in
@@ -348,7 +349,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp)
| Thesis (For rec_occ) ->
if not (Id.List.mem rec_occ pat_vars) then
- errorlabstrm "suppose it is"
+ user_err ~hdr:"suppose it is"
(str "Variable " ++ Nameops.pr_id rec_occ ++
str " does not occur in pattern.");
Glob_term.GSort(Loc.ghost,GProp)
@@ -358,10 +359,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
let rids=ref ([],pat_vars) in
let npatt= deanonymize rids patt in
List.rev (fst !rids),npatt in
- let term2 =
- GLetIn(Loc.ghost,Anonymous,
- GCast(Loc.ghost,glob_of_pat npatt,
- CastConv app_ind),term1) in
+ let term2=GLetIn(Loc.ghost,Anonymous,glob_of_pat npatt,Some app_ind,term1) in
let term3=List.fold_right let_in_one_alias aliases term2 in
let term4=List.fold_right prod_one_id loc_ids term3 in
let term5=List.fold_right prod_one_hyp params term4 in
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index d30fcf6033..deb2ede1d5 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Ltac_plugin
open CErrors
open Util
open Pp
@@ -32,6 +33,9 @@ open Misctypes
open Sigma.Notations
open Context.Named.Declaration
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
(* Strictness option *)
let clear ids { it = goal; sigma } =
@@ -43,7 +47,7 @@ let clear ids { it = goal; sigma } =
let (hyps, concl) =
try Evarutil.clear_hyps_in_evi env evdref sign cl ids
with Evarutil.ClearDependencyError (id, _) ->
- errorlabstrm "" (str "Cannot clear " ++ pr_id id)
+ user_err (str "Cannot clear " ++ pr_id id)
in
let sigma = !evdref in
let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
@@ -247,7 +251,7 @@ let close_previous_case pts =
let filter_hyps f gls =
let filter_aux id =
- let id = get_id id in
+ let id = NamedDecl.get_id id in
if f id then
tclIDTAC
else
@@ -357,8 +361,7 @@ let enstack_subsubgoals env se stack gls=
let nlast=succ last in
let (llast,holes,metas) =
meta_aux nlast (mkMeta nlast :: lenv) q in
- let open Context.Rel.Declaration in
- (llast,holes,(nlast,special_nf gls (substl lenv (get_type decl)))::metas) in
+ (llast,holes,(nlast,special_nf gls (substl lenv (RelDecl.get_type decl)))::metas) in
let (nlast,holes,nmetas) =
meta_aux se.se_last_meta [] (List.rev rc) in
let refiner = applist (appterm,List.rev holes) in
@@ -821,9 +824,8 @@ let define_tac id args body gls =
let cast_tac id_or_thesis typ gls =
match id_or_thesis with
- This id ->
- let body = pf_get_hyp gls id |> get_value in
- Proofview.V82.of_tactic (convert_hyp (of_tuple (id,body,typ))) gls
+ | This id ->
+ Proofview.V82.of_tactic (id |> pf_get_hyp gls |> NamedDecl.set_id id |> NamedDecl.set_type typ |> convert_hyp) gls
| Thesis (For _ ) ->
error "\"thesis for ...\" is not applicable here."
| Thesis Plain ->
@@ -1082,12 +1084,12 @@ let thesis_for obj typ per_info env=
let cind,all_args=decompose_app typ in
let ind,u = destInd cind in
let _ = if not (eq_ind ind per_info.per_ind) then
- errorlabstrm "thesis_for"
+ user_err ~hdr:"thesis_for"
((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
str"cannot give an induction hypothesis (wrong inductive type).") in
let params,args = List.chop per_info.per_nparams all_args in
let _ = if not (List.for_all2 eq_constr params per_info.per_params) then
- errorlabstrm "thesis_for"
+ user_err ~hdr:"thesis_for"
((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
str "cannot give an induction hypothesis (wrong parameters).") in
let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 6c17dcc4f1..a71d20f0dc 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -10,6 +10,7 @@
DECLARE PLUGIN "decl_mode_plugin"
+open Ltac_plugin
open Compat
open Pp
open Decl_expr
@@ -19,7 +20,7 @@ open Vernacexpr
open Tok (* necessary for camlp4 *)
open Pcoq.Constr
-open Pcoq.Tactic
+open Pltac
open Ppdecl_proof
let pr_goal gs =
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 59a0bb5a2d..f5de638ed2 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Ltac_plugin
open CErrors
open Pp
open Decl_expr
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 18:13:05 +0000