aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml6
-rw-r--r--proofs/clenvtac.ml2
-rw-r--r--proofs/evar_refiner.ml4
-rw-r--r--proofs/logic.ml6
-rw-r--r--proofs/pfedit.ml32
-rw-r--r--proofs/proof.ml28
-rw-r--r--proofs/proof_global.ml36
-rw-r--r--proofs/redexpr.ml8
-rw-r--r--proofs/refiner.ml16
-rw-r--r--proofs/tacmach.ml10
-rw-r--r--proofs/tacmach.mli4
11 files changed, 78 insertions, 74 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 853410db8..0a90e0dbd 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -72,7 +72,7 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
exception NotExtensibleClause
let clenv_push_prod cl =
- let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+ let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
let rec clrec typ = match kind_of_term typ with
| Cast (t,_,_) -> clrec t
| Prod (na,t,u) ->
@@ -663,7 +663,7 @@ let evar_of_binder holes = function
try
let h = List.nth holes (pred n) in
h.hole_evar
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
errorlabstrm "" (str "No such binder.")
let define_with_type sigma env ev c =
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index da2eee32a..04a2eb487 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -125,5 +125,5 @@ let unify ?(flags=fail_quick_unif_flags) m =
try
let evd' = w_unify env evd CONV ~flags m n in
Proofview.Unsafe.tclEVARSADVANCE evd'
- with e when Errors.noncritical e -> Proofview.tclZERO e
+ with e when CErrors.noncritical e -> Proofview.tclZERO e
end }
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 3192a6a29..58b881174 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Evd
@@ -52,7 +52,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
Pretyping.expand_evars = true } in
try Pretyping.understand_ltac flags
env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
let loc = Glob_ops.loc_of_glob_constr rawc in
user_err_loc
(loc,"", str "Instance is not well-typed in the environment of " ++
diff --git a/proofs/logic.ml b/proofs/logic.ml
index fd8a70c65..aa0b9bac6 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -59,7 +59,7 @@ let is_unification_error = function
| _ -> false
let catchable_exception = function
- | Errors.UserError _ | TypeError _
+ | CErrors.UserError _ | TypeError _
| RefinerError _ | Indrec.RecursionSchemeError _
| Nametab.GlobalizationError _
(* reduction errors *)
@@ -463,7 +463,7 @@ and mk_hdgoals sigma goal goalacc trm =
and mk_arggoals sigma goal goalacc funty allargs =
let foldmap (goalacc, funty, sigma) harg =
- let t = whd_betadeltaiota (Goal.V82.env sigma goal) sigma funty in
+ let t = whd_all (Goal.V82.env sigma goal) sigma funty in
let rec collapse t = match kind_of_term t with
| LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
| _ -> t
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index bf1da8ac0..e4bae2012 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -39,7 +39,7 @@ let cook_this_proof p =
match p with
| { Proof_global.id;entries=[constr];persistence;universes } ->
(id,(constr,universes,persistence))
- | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
+ | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
let cook_proof () =
cook_this_proof (fst
@@ -59,9 +59,9 @@ let get_universe_binders () =
Proof_global.get_universe_binders ()
exception NoSuchGoal
-let _ = Errors.register_handler begin function
- | NoSuchGoal -> Errors.error "No such goal."
- | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+ | NoSuchGoal -> CErrors.error "No such goal."
+ | _ -> raise CErrors.Unhandled
end
let get_nth_V82_goal i =
let p = Proof_global.give_me_the_proof () in
@@ -76,12 +76,12 @@ let get_goal_context_gen i =
let get_goal_context i =
try get_goal_context_gen i
- with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
- | NoSuchGoal -> Errors.error "No such goal."
+ with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
+ | NoSuchGoal -> CErrors.error "No such goal."
let get_current_goal_context () =
try get_goal_context_gen 1
- with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
+ with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
| NoSuchGoal ->
(* spiwack: returning empty evar_map, since if there is no goal, under focus,
there is no accessible evar either *)
@@ -102,7 +102,7 @@ let get_current_context () =
let current_proof_statement () =
match Proof_global.V82.get_current_initial_conclusions () with
| (id,([concl],strength)) -> id,strength,concl
- | _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement")
+ | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement")
let solve ?with_end_tac gi info_lvl tac pr =
try
@@ -127,11 +127,11 @@ let solve ?with_end_tac gi info_lvl tac pr =
in
(p,status)
with
- | Proof_global.NoCurrentProof -> Errors.error "No focused proof"
+ | Proof_global.NoCurrentProof -> CErrors.error "No focused proof"
| CList.IndexOutOfRange ->
match gi with
| Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
- Errors.errorlabstrm "" msg
+ CErrors.errorlabstrm "" msg
| _ -> assert false
let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
@@ -157,7 +157,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
delete_current_proof ();
const, status, fst univs
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
delete_current_proof ();
iraise reraise
@@ -188,7 +188,7 @@ let refine_by_tactic env sigma ty tac =
try Proof.run_tactic env tac prf
with Logic_monad.TacticFailure e as src ->
(** Catch the inner error of the monad tactic *)
- let (_, info) = Errors.push src in
+ let (_, info) = CErrors.push src in
iraise (e, info)
in
(** Plug back the retrieved sigma *)
@@ -215,7 +215,7 @@ let refine_by_tactic env sigma ty tac =
(* Support for resolution of evars in tactic interpretation, including
resolution by application of tactics *)
-let implicit_tactic = ref None
+let implicit_tactic = Summary.ref None ~name:"implicit-tactic"
let declare_implicit_tactic tac = implicit_tactic := Some tac
@@ -228,10 +228,12 @@ let solve_by_implicit_tactic env sigma evk =
when
Context.Named.equal (Environ.named_context_of_val evi.evar_hyps)
(Environ.named_context env) ->
- let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in
+ let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError ("",Pp.str"Proof is not complete."))) []) in
(try
+ let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
+ if Evarutil.has_undefined_evars sigma c then raise Exit;
let (ans, _, _) =
- build_by_tactic env (Evd.evar_universe_context sigma) evi.evar_concl tac in
+ build_by_tactic env (Evd.evar_universe_context sigma) c tac in
ans
with e when Logic.catchable_exception e -> raise Exit)
| _ -> raise Exit
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 86af420dc..5fe29653d 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -64,17 +64,17 @@ exception NoSuchGoals of int * int
exception FullyUnfocused
-let _ = Errors.register_handler begin function
+let _ = CErrors.register_handler begin function
| CannotUnfocusThisWay ->
- Errors.error "This proof is focused, but cannot be unfocused this way"
+ CErrors.error "This proof is focused, but cannot be unfocused this way"
| NoSuchGoals (i,j) when Int.equal i j ->
- Errors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
+ CErrors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
| NoSuchGoals (i,j) ->
- Errors.errorlabstrm "Focus" Pp.(
+ CErrors.errorlabstrm "Focus" Pp.(
str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
)
- | FullyUnfocused -> Errors.error "The proof is not focused"
- | _ -> raise Errors.Unhandled
+ | FullyUnfocused -> CErrors.error "The proof is not focused"
+ | _ -> raise CErrors.Unhandled
end
let check_cond_kind c k =
@@ -300,12 +300,12 @@ exception UnfinishedProof
exception HasShelvedGoals
exception HasGivenUpGoals
exception HasUnresolvedEvar
-let _ = Errors.register_handler begin function
- | UnfinishedProof -> Errors.error "Some goals have not been solved."
- | HasShelvedGoals -> Errors.error "Some goals have been left on the shelf."
- | HasGivenUpGoals -> Errors.error "Some goals have been given up."
- | HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated."
- | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+ | UnfinishedProof -> CErrors.error "Some goals have not been solved."
+ | HasShelvedGoals -> CErrors.error "Some goals have been left on the shelf."
+ | HasGivenUpGoals -> CErrors.error "Some goals have been given up."
+ | HasUnresolvedEvar -> CErrors.error "Some existential variables are uninstantiated."
+ | _ -> raise CErrors.Unhandled
end
let return p =
@@ -397,9 +397,9 @@ module V82 = struct
let evl = Evarutil.non_instantiated sigma in
let evl = Evar.Map.bindings evl in
if (n <= 0) then
- Errors.error "incorrect existential variable index"
+ CErrors.error "incorrect existential variable index"
else if CList.length evl < n then
- Errors.error "not so many uninstantiated existential variables"
+ CErrors.error "not so many uninstantiated existential variables"
else
CList.nth evl (n-1)
in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 61fe34750..7605f6387 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -34,7 +34,7 @@ let proof_modes = Hashtbl.create 6
let find_proof_mode n =
try Hashtbl.find proof_modes n
with Not_found ->
- Errors.error (Format.sprintf "No proof mode named \"%s\"." n)
+ CErrors.error (Format.sprintf "No proof mode named \"%s\"." n)
let register_proof_mode ({name = n} as m) =
Hashtbl.add proof_modes n (CEphemeron.create m)
@@ -122,15 +122,15 @@ let push a l = l := a::!l;
update_proof_mode ()
exception NoSuchProof
-let _ = Errors.register_handler begin function
- | NoSuchProof -> Errors.error "No such proof."
- | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+ | NoSuchProof -> CErrors.error "No such proof."
+ | _ -> raise CErrors.Unhandled
end
exception NoCurrentProof
-let _ = Errors.register_handler begin function
- | NoCurrentProof -> Errors.error "No focused proof (No proof-editing in progress)."
- | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+ | NoCurrentProof -> CErrors.error "No focused proof (No proof-editing in progress)."
+ | _ -> raise CErrors.Unhandled
end
(*** Proof Global manipulation ***)
@@ -190,7 +190,7 @@ let check_no_pending_proof () =
if not (there_are_pending_proofs ()) then
()
else begin
- Errors.error (Pp.string_of_ppcmds
+ CErrors.error (Pp.string_of_ppcmds
(str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++
str"Use \"Abort All\" first or complete proof(s)."))
end
@@ -202,7 +202,7 @@ let discard (loc,id) =
let n = List.length !pstates in
discard_gen id;
if Int.equal (List.length !pstates) n then
- Errors.user_err_loc
+ CErrors.user_err_loc
(loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
let discard_current () =
@@ -296,7 +296,7 @@ let set_used_variables l =
| [] -> raise NoCurrentProof
| p :: rest ->
if not (Option.is_empty p.section_vars) then
- Errors.error "Used section variables can be declared only once";
+ CErrors.error "Used section variables can be declared only once";
pstates := { p with section_vars = Some ctx} :: rest;
ctx, to_clear
@@ -408,7 +408,7 @@ let return_proof ?(allow_partial=false) () =
let evd =
let error s =
let prf = str " (in proof " ++ Id.print pid ++ str ")" in
- raise (Errors.UserError("last tactic before Qed",s ++ prf))
+ raise (CErrors.UserError("last tactic before Qed",s ++ prf))
in
try Proof.return proof with
| Proof.UnfinishedProof ->
@@ -515,12 +515,12 @@ module Bullet = struct
exception FailedBullet of t * suggestion
let _ =
- Errors.register_handler
+ CErrors.register_handler
(function
| FailedBullet (b,sugg) ->
let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
- Errors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg)
- | _ -> raise Errors.Unhandled)
+ CErrors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg)
+ | _ -> raise CErrors.Unhandled)
(* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
@@ -633,7 +633,7 @@ module Bullet = struct
current_behavior :=
try Hashtbl.find behaviors n
with Not_found ->
- Errors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
+ CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
end
}
@@ -681,9 +681,9 @@ let parse_goal_selector = function
let err_msg = "The default selector must be \"all\" or a natural number." in
begin try
let i = int_of_string i in
- if i < 0 then Errors.error err_msg;
+ if i < 0 then CErrors.error err_msg;
Vernacexpr.SelectNth i
- with Failure _ -> Errors.error err_msg
+ with Failure _ -> CErrors.error err_msg
end
let _ =
@@ -712,7 +712,7 @@ type state = pstate list
let freeze ~marshallable =
match marshallable with
| `Yes ->
- Errors.anomaly (Pp.str"full marshalling of proof state not supported")
+ CErrors.anomaly (Pp.str"full marshalling of proof state not supported")
| `Shallow -> !pstates
| `No -> !pstates
let unfreeze s = pstates := s; update_proof_mode ()
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index ee5591521..8a9ce4f94 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -17,7 +17,7 @@ open Genredexpr
open Pattern
open Reductionops
open Tacred
-open Closure
+open CClosure
open RedFlags
open Libobject
open Misctypes
@@ -146,7 +146,9 @@ let make_flag_constant = function
let make_flag env f =
let red = no_red in
let red = if f.rBeta then red_add red fBETA else red in
- let red = if f.rIota then red_add red fIOTA else red in
+ let red = if f.rMatch then red_add red fMATCH else red in
+ let red = if f.rFix then red_add red fFIX else red in
+ let red = if f.rCofix then red_add red fCOFIX else red in
let red = if f.rZeta then red_add red fZETA else red in
let red =
if f.rDelta then (* All but rConst *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 23433692c..ebd30820b 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Evd
open Environ
@@ -240,8 +240,8 @@ let tclORELSE0 t1 t2 g =
try
t1 g
with (* Breakpoint *)
- | e when Errors.noncritical e ->
- let e = Errors.push e in catch_failerror e; t2 g
+ | e when CErrors.noncritical e ->
+ let e = CErrors.push e in catch_failerror e; t2 g
(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
then applies t2 *)
@@ -253,8 +253,8 @@ let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2
let tclORELSE_THEN t1 t2then t2else gls =
match
try Some(tclPROGRESS t1 gls)
- with e when Errors.noncritical e ->
- let e = Errors.push e in catch_failerror e; None
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in catch_failerror e; None
with
| None -> t2else gls
| Some sgl ->
@@ -284,12 +284,12 @@ let ite_gen tcal tac_if continue tac_else gl=
try
tac_else gl
with
- e' when Errors.noncritical e' -> iraise e in
+ e' when CErrors.noncritical e' -> iraise e in
try
tcal tac_if0 continue gl
with (* Breakpoint *)
- | e when Errors.noncritical e ->
- let e = Errors.push e in catch_failerror e; tac_else0 e gl
+ | e when CErrors.noncritical e ->
+ let e = CErrors.push e in catch_failerror e; tac_else0 e gl
(* Try the first tactic and, if it succeeds, continue with
the second one, and if it fails, use the third one *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 8c0b4ba98..50984c48e 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -84,7 +84,7 @@ let pf_eapply f gls x =
let pf_reduce = pf_apply
let pf_e_reduce = pf_apply
-let pf_whd_betadeltaiota = pf_reduce whd_betadeltaiota
+let pf_whd_all = pf_reduce whd_all
let pf_hnf_constr = pf_reduce hnf_constr
let pf_nf = pf_reduce simpl
let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota)
@@ -101,7 +101,7 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value_in env)
let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind
-let pf_hnf_type_of gls = pf_whd_betadeltaiota gls % pf_get_type_of gls
+let pf_hnf_type_of gls = pf_whd_all gls % pf_get_type_of gls
let pf_is_matching = pf_apply Constr_matching.is_matching_conv
let pf_matches = pf_apply Constr_matching.matches_conv
@@ -219,7 +219,7 @@ module New = struct
let sigma = project gl in
nf_evar sigma concl
- let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
+ let pf_whd_all gl t = pf_apply whd_all gl t
let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t
@@ -228,11 +228,11 @@ module New = struct
let pf_hnf_constr gl t = pf_apply hnf_constr gl t
let pf_hnf_type_of gl t =
- pf_whd_betadeltaiota gl (pf_get_type_of gl t)
+ pf_whd_all gl (pf_get_type_of gl t)
let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
- let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
+ let pf_whd_all gl t = pf_apply whd_all gl t
let pf_compute gl t = pf_apply compute gl t
let pf_nf_evar gl t = nf_evar (project gl) t
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 182433cb3..100ed1522 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -63,7 +63,7 @@ val pf_e_reduce :
(env -> evar_map -> constr -> evar_map * constr) ->
goal sigma -> constr -> evar_map * constr
-val pf_whd_betadeltaiota : goal sigma -> constr -> constr
+val pf_whd_all : goal sigma -> constr -> constr
val pf_hnf_constr : goal sigma -> constr -> constr
val pf_nf : goal sigma -> constr -> constr
val pf_nf_betaiota : goal sigma -> constr -> constr
@@ -127,7 +127,7 @@ module New : sig
val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
- val pf_whd_betadeltaiota : ('a, 'r) Proofview.Goal.t -> constr -> constr
+ val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr
val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr
val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 10:53:45 +0000