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.ml14
-rw-r--r--plugins/decl_mode/decl_mode.ml2
-rw-r--r--plugins/decl_mode/decl_mode_plugin.mlpack (renamed from plugins/decl_mode/decl_mode_plugin.mllib)1
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml48
-rw-r--r--plugins/decl_mode/g_decl_mode.ml48
-rw-r--r--plugins/decl_mode/ppdecl_proof.ml2
6 files changed, 42 insertions, 33 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 34307a358f..f68c01b18b 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Constrexpr
@@ -90,8 +90,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) ->
@@ -153,8 +153,8 @@ let interp_constr check_sort env sigma c =
fst (understand env sigma (fst c))
let special_whd env =
- let infos=Closure.create_clos_infos Closure.betadeltaiota env in
- (fun t -> Closure.whd_val infos (Closure.inject t))
+ let infos=CClosure.create_clos_infos CClosure.all env in
+ (fun t -> CClosure.whd_val infos (CClosure.inject t))
let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq))
@@ -328,7 +328,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 +348,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)
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index f9399d6824..92d4089015 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -9,7 +9,7 @@
open Names
open Term
open Evd
-open Errors
+open CErrors
open Util
let daimon_flag = ref false
diff --git a/plugins/decl_mode/decl_mode_plugin.mllib b/plugins/decl_mode/decl_mode_plugin.mlpack
index 39342dbd1c..1b84a0790f 100644
--- a/plugins/decl_mode/decl_mode_plugin.mllib
+++ b/plugins/decl_mode/decl_mode_plugin.mlpack
@@ -3,4 +3,3 @@ Decl_interp
Decl_proof_instr
Ppdecl_proof
G_decl_mode
-Decl_mode_plugin_mod
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 3fa600ac29..e19dc86c45 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Pp
open Evd
@@ -32,6 +32,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 +46,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
@@ -60,7 +63,7 @@ let _ =
declare_bool_option
{ optsync = true;
optdepr = false;
- optname = "strict mode";
+ optname = "strict proofs";
optkey = ["Strict";"Proofs"];
optread = get_strictness;
optwrite = set_strictness }
@@ -84,12 +87,12 @@ let tcl_erase_info gls =
tcl_change_info_gen info_gen gls
let special_whd gl=
- let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in
- (fun t -> Closure.whd_val infos (Closure.inject t))
+ let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in
+ (fun t -> CClosure.whd_val infos (CClosure.inject t))
let special_nf gl=
- let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in
- (fun t -> Closure.norm_val infos (Closure.inject t))
+ let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in
+ (fun t -> CClosure.norm_val infos (CClosure.inject t))
let is_good_inductive env ind =
let mib,oib = Inductive.lookup_mind_specif env ind in
@@ -247,7 +250,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
@@ -277,12 +280,16 @@ let prepare_goal items gls =
filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls
let my_automation_tac = ref
- (Proofview.tclZERO (Errors.make_anomaly (Pp.str"No automation registered")))
+ (Proofview.tclZERO (CErrors.make_anomaly (Pp.str"No automation registered")))
let register_automation_tac tac = my_automation_tac:= tac
let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_automation_tac)
+let warn_insufficient_justification =
+ CWarnings.create ~name:"declmode-insufficient-justification" ~category:"declmode"
+ (fun () -> strbrk "Insufficient justification.")
+
let justification tac gls=
tclORELSE
(tclSOLVE [tclTHEN tac (Proofview.V82.of_tactic assumption)])
@@ -291,7 +298,7 @@ let justification tac gls=
error "Insufficient justification."
else
begin
- Feedback.msg_warning (str "Insufficient justification.");
+ warn_insufficient_justification ();
daimon_tac gls
end) gls
@@ -353,8 +360,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
@@ -411,7 +417,7 @@ let find_subsubgoal c ctyp skip submetas gls =
se.se_meta submetas se.se_meta_list}
else
dfs (pred n)
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
begin
enstack_subsubgoals env se stack gls;
dfs n
@@ -817,9 +823,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 ->
@@ -1078,12 +1083,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
@@ -1219,6 +1224,9 @@ let hrec_for fix_id per_info gls obj_id =
let hd2 = applist (mkVar fix_id,args@[obj]) in
compose_lam rc (Reductionops.whd_beta gls.sigma hd2)
+let warn_missing_case =
+ CWarnings.create ~name:"declmode-missing-case" ~category:"declmode"
+ (fun () -> strbrk "missing case")
let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
match tree, objs with
@@ -1293,8 +1301,8 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
end;
match bro with
None ->
- Feedback.msg_warning (str "missing case");
- tacnext (mkMeta 1)
+ warn_missing_case ();
+ tacnext (mkMeta 1)
| Some (sub_ids,tree) ->
let br_args =
List.filter
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 78a95143df..18a35c6cfb 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -8,6 +8,8 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
+DECLARE PLUGIN "decl_mode_plugin"
+
open Compat
open Pp
open Decl_expr
@@ -17,7 +19,7 @@ open Vernacexpr
open Tok (* necessary for camlp4 *)
open Pcoq.Constr
-open Pcoq.Tactic
+open Pltac
open Ppdecl_proof
let pr_goal gs =
@@ -56,7 +58,7 @@ let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }=
let vernac_decl_proof () =
let pf = Proof_global.give_me_the_proof () in
if Proof.is_done pf then
- Errors.error "Nothing left to prove here."
+ CErrors.error "Nothing left to prove here."
else
begin
Decl_proof_instr.go_to_proof_mode () ;
@@ -98,7 +100,7 @@ let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
let classify_proof_instr = function
| { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow
- | _ -> VtProofStep false, VtLater
+ | _ -> Vernac_classifier.classify_as_proofstep
(* We use the VERNAC EXTEND facility with a custom non-terminal
to populate [proof_mode] with a new toplevel interpreter.
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 4c71f04107..59a0bb5a2d 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Pp
open Decl_expr
open Names
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:06:28 +0000