aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml8
-rw-r--r--proofs/evar_refiner.ml2
-rw-r--r--proofs/goal.ml2
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--proofs/proof_global.ml31
-rw-r--r--proofs/proof_global.mli4
-rw-r--r--proofs/proof_using.ml8
-rw-r--r--proofs/redexpr.ml2
-rw-r--r--proofs/refine.ml23
-rw-r--r--proofs/refine.mli6
11 files changed, 50 insertions, 40 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 605914a01..9e0a2a03e 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -416,7 +416,7 @@ let qhyp_eq h1 h2 = match h1, h2 with
| _ -> false
let check_bindings bl =
- match List.duplicates qhyp_eq (List.map pi2 bl) with
+ match List.duplicates qhyp_eq (List.map (fun x -> fst (snd x)) bl) with
| NamedHyp s :: _ ->
user_err
(str "The variable " ++ pr_id s ++
@@ -512,7 +512,7 @@ let clenv_match_args bl clenv =
let mvs = clenv_independent clenv in
check_bindings bl;
List.fold_left
- (fun clenv (loc,b,c) ->
+ (fun clenv (loc,(b,c)) ->
let k = meta_of_binder clenv loc mvs b in
if meta_defined clenv.evd k then
if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv
@@ -676,7 +676,7 @@ let define_with_type sigma env ev c =
let t = Retyping.get_type_of env sigma ev in
let ty = Retyping.get_type_of env sigma c in
let j = Environ.make_judge c ty in
- let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in
+ let (sigma, j) = Coercion.inh_conv_coerce_to true env sigma j t in
let (ev, _) = destEvar sigma ev in
let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in
sigma
@@ -711,7 +711,7 @@ let solve_evar_clause env sigma hyp_only clause = function
error_not_right_number_missing_arguments len
| ExplicitBindings lbind ->
let () = check_bindings lbind in
- let fold sigma (_, binder, c) =
+ let fold sigma (_, (binder, c)) =
let ev = evar_of_binder clause.cl_holes binder in
define_with_type sigma env ev c
in
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 8367c09b8..b9c925796 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -56,7 +56,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc
with e when CErrors.noncritical e ->
let loc = Glob_ops.loc_of_glob_constr rawc in
- user_err ~loc
+ user_err ?loc
(str "Instance is not well-typed in the environment of " ++
Termops.pr_existential_key sigma evk ++ str ".")
in
diff --git a/proofs/goal.ml b/proofs/goal.ml
index fc8e635a0..5a717f166 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -68,7 +68,7 @@ module V82 = struct
Evd.evar_concl = concl;
Evd.evar_filter = Evd.Filter.identity;
Evd.evar_body = Evd.Evar_empty;
- Evd.evar_source = (Loc.ghost,Evar_kinds.GoalEvar);
+ Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
Evd.evar_candidates = None;
Evd.evar_extra = extra }
in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7e8ed31d1..92b4e788a 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -15,7 +15,7 @@ open Evd
let use_unification_heuristics_ref = ref true
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname = "Solve unification constraints at every \".\"";
Goptions.optkey = ["Solve";"Unification";"Constraints"];
Goptions.optread = (fun () -> !use_unification_heuristics_ref);
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 7622a8776..1bf65b8ae 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -130,7 +130,7 @@ val set_end_tac : Genarg.glob_generic_argument -> unit
(** [set_used_variables l] declares that section variables [l] will be
used in the proof *)
val set_used_variables :
- Id.t list -> Context.Named.t * (Loc.t * Names.Id.t) list
+ Id.t list -> Context.Named.t * Names.Id.t Loc.located list
val get_used_variables : unit -> Context.Named.t option
(** {6 Universe binders } *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5f4a7766f..95aee72cb 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -52,8 +52,7 @@ let get_default_proof_mode_name () =
(CEphemeron.default !default_proof_mode standard).name
let _ =
- Goptions.declare_string_option {Goptions.
- optsync = true ;
+ Goptions.(declare_string_option {
optdepr = false;
optname = "default proof mode" ;
optkey = ["Default";"Proof";"Mode"] ;
@@ -63,7 +62,7 @@ let _ =
optwrite = begin fun n ->
default_proof_mode := find_proof_mode n
end
- }
+ })
(*** Proof Global Environment ***)
@@ -82,7 +81,7 @@ type proof_object = {
type proof_ending =
| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
| Proved of Vernacexpr.opacity_flag *
- (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+ Vernacexpr.lident option *
proof_object
type proof_terminator = proof_ending -> unit
type closed_proof = proof_object * proof_terminator
@@ -207,7 +206,7 @@ let discard (loc,id) =
let n = List.length !pstates in
discard_gen id;
if Int.equal (List.length !pstates) n then
- CErrors.user_err ~loc
+ CErrors.user_err ?loc
~hdr:"Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ())
let discard_current () =
@@ -268,8 +267,7 @@ let get_universe_binders () = (cur_pstate ()).universe_binders
let proof_using_auto_clear = ref false
let _ = Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "Proof using Clear Unused";
Goptions.optkey = ["Proof";"Using";"Clear";"Unused"];
Goptions.optread = (fun () -> !proof_using_auto_clear);
@@ -287,13 +285,13 @@ let set_used_variables l =
match entry with
| LocalAssum (x,_) ->
if Id.Set.mem x all_safe then orig
- else (ctx, all_safe, (Loc.ghost,x)::to_clear)
+ else (ctx, all_safe, (Loc.tag x)::to_clear)
| LocalDef (x,bo, ty) as decl ->
if Id.Set.mem x all_safe then orig else
let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
if Id.Set.subset vars all_safe
then (decl :: ctx, Id.Set.add x all_safe, to_clear)
- else (ctx, all_safe, (Loc.ghost,x) :: to_clear) in
+ else (ctx, all_safe, (Loc.tag x) :: to_clear) in
let ctx, _, to_clear =
Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in
let to_clear = if !proof_using_auto_clear then to_clear else [] in
@@ -516,7 +514,7 @@ module Bullet = struct
| NeedClosingBrace -> str"Try unfocusing with \"}\"."
| NoBulletInUse -> assert false (* This should never raise an error. *)
| ProofFinished -> str"No more subgoals."
- | Suggest b -> str"Bullet " ++ pr_bullet b ++ str" is mandatory here."
+ | Suggest b -> str"Expecting " ++ pr_bullet b ++ str"."
| Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished."
exception FailedBullet of t * suggestion
@@ -525,7 +523,7 @@ module Bullet = struct
CErrors.register_handler
(function
| FailedBullet (b,sugg) ->
- let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
+ let prefix = str"Wrong bullet " ++ pr_bullet b ++ str": " in
CErrors.user_err ~hdr:"Focus" (prefix ++ suggest_on_error sugg)
| _ -> raise CErrors.Unhandled)
@@ -628,8 +626,7 @@ module Bullet = struct
let current_behavior = ref Strict.strict
let _ =
- Goptions.declare_string_option {Goptions.
- optsync = true;
+ Goptions.(declare_string_option {
optdepr = false;
optname = "bullet behavior";
optkey = ["Bullet";"Behavior"];
@@ -642,7 +639,7 @@ module Bullet = struct
with Not_found ->
CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
end
- }
+ })
let put p b =
(!current_behavior).put p b
@@ -696,9 +693,7 @@ let parse_goal_selector = function
end
let _ =
- Goptions.declare_string_option {Goptions.
- optsync = true ;
- optdepr = false;
+ Goptions.(declare_string_option{optdepr = false;
optname = "default goal selector" ;
optkey = ["Default";"Goal";"Selector"] ;
optread = begin fun () ->
@@ -708,7 +703,7 @@ let _ =
optwrite = begin fun n ->
default_goal_selector := parse_goal_selector n
end
- }
+ })
module V82 = struct
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 6bb6f5e2c..52bbd9ac5 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -70,7 +70,7 @@ type proof_ending =
| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
proof_universes
| Proved of Vernacexpr.opacity_flag *
- (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+ Vernacexpr.lident option *
proof_object
type proof_terminator
type closed_proof = proof_object * proof_terminator
@@ -140,7 +140,7 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit
* (w.r.t. type dependencies and let-ins covered by it) + a list of
* ids to be cleared *)
val set_used_variables :
- Names.Id.t list -> Context.Named.t * (Loc.t * Names.Id.t) list
+ Names.Id.t list -> Context.Named.t * Names.Id.t Loc.located list
val get_used_variables : unit -> Context.Named.t option
val get_universe_binders : unit -> universe_binders option
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index 2c489d6de..f701f7cfe 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -76,7 +76,7 @@ and full_set env =
List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
let process_expr env e ty =
- let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in
+ let ty_expr = SsSingl(Loc.tag @@ Id.of_string "Type") in
let v_ty = process_expr env ty_expr ty in
let s = Id.Set.union v_ty (process_expr env e ty) in
Id.Set.elements s
@@ -144,8 +144,7 @@ let value = ref false
let _ =
Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "suggest Proof using";
Goptions.optkey = ["Suggest";"Proof";"Using"];
Goptions.optread = (fun () -> !value);
@@ -159,8 +158,7 @@ let value = ref None
let _ =
Goptions.declare_stringopt_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "default value for Proof using";
Goptions.optkey = ["Default";"Proof";"Using"];
Goptions.optread = (fun () -> !value);
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index cb3538422..7cd526843 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -52,7 +52,7 @@ let strong_cbn flags =
let simplIsCbn = ref (false)
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname =
"Plug the simpl tactic to the new cbn mechanism";
Goptions.optkey = ["SimplIsCbn"];
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 1ee6e0ca5..63ae41075 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -70,8 +70,7 @@ let add_side_effect env = function
let add_side_effects env effects =
List.fold_left (fun env eff -> add_side_effect env eff) env effects
-let make_refine_enter ?(unsafe = true) f =
- { enter = fun gl ->
+let generic_refine ?(unsafe = true) f gl =
let gl = Proofview.Goal.assume gl in
let sigma = Proofview.Goal.sigma gl in
let sigma = Sigma.to_evar_map sigma in
@@ -82,7 +81,10 @@ let make_refine_enter ?(unsafe = true) f =
let prev_future_goals = Evd.future_goals sigma in
let prev_principal_goal = Evd.principal_future_goal sigma in
(** Create the refinement term *)
- let ((v,c), sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
+ Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () ->
+ f >>= fun (v, c) ->
+ Proofview.tclEVARMAP >>= fun sigma ->
+ Proofview.V82.wrap_exceptions begin fun () ->
let evs = Evd.future_goals sigma in
let evkmain = Evd.principal_future_goal sigma in
(** Redo the effects in sigma in the monad's env *)
@@ -122,7 +124,18 @@ let make_refine_enter ?(unsafe = true) f =
Proofview.Unsafe.tclEVARS sigma <*>
Proofview.Unsafe.tclSETGOALS comb <*>
Proofview.tclUNIT v
- }
+ end
+
+let lift c =
+ Proofview.tclEVARMAP >>= fun sigma ->
+ Proofview.V82.wrap_exceptions begin fun () ->
+ let Sigma (c, sigma, _) = c.run (Sigma.Unsafe.of_evar_map sigma) in
+ Proofview.Unsafe.tclEVARS (Sigma.to_evar_map sigma) >>= fun () ->
+ Proofview.tclUNIT c
+ end
+
+let make_refine_enter ?unsafe f =
+ { enter = fun gl -> generic_refine ?unsafe (lift f) gl }
let refine_one ?(unsafe = true) f =
Proofview.Goal.enter_one (make_refine_enter ~unsafe f)
@@ -137,7 +150,7 @@ let with_type env evd c t =
let my_type = Retyping.get_type_of env evd c in
let j = Environ.make_judge c my_type in
let (evd,j') =
- Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
+ Coercion.inh_conv_coerce_to true env evd j t
in
evd , j'.Environ.uj_val
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 1a254d578..5098f246a 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -31,7 +31,11 @@ val refine : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
type-checked beforehand. *)
val refine_one : ?unsafe:bool -> ('a * EConstr.t) Sigma.run -> 'a tactic
-(** A generalization of [refine] which assumes exactly one goal under focus *)
+(** A variant of [refine] which assumes exactly one goal under focus *)
+
+val generic_refine : ?unsafe:bool -> ('a * EConstr.t) tactic ->
+ ([ `NF ], 'r) Proofview.Goal.t -> 'a tactic
+(** The general version of refine. *)
(** {7 Helper functions} *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 21:08:37 +0000