diff options
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/clenv.ml | 16 | ||||
-rw-r--r-- | proofs/evar_refiner.ml | 6 | ||||
-rw-r--r-- | proofs/goal.ml | 2 | ||||
-rw-r--r-- | proofs/logic.ml | 8 | ||||
-rw-r--r-- | proofs/pfedit.ml | 14 | ||||
-rw-r--r-- | proofs/pfedit.mli | 2 | ||||
-rw-r--r-- | proofs/proof.ml | 16 | ||||
-rw-r--r-- | proofs/proof_global.ml | 47 | ||||
-rw-r--r-- | proofs/proof_global.mli | 4 | ||||
-rw-r--r-- | proofs/proof_using.ml | 8 | ||||
-rw-r--r-- | proofs/redexpr.ml | 4 | ||||
-rw-r--r-- | proofs/refine.ml | 23 | ||||
-rw-r--r-- | proofs/refine.mli | 6 | ||||
-rw-r--r-- | proofs/refiner.ml | 6 | ||||
-rw-r--r-- | proofs/tacmach.ml | 4 | ||||
-rw-r--r-- | proofs/tacmach.mli | 2 |
16 files changed, 88 insertions, 80 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 605914a01..d6ed201d8 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -157,13 +157,13 @@ let error_incompatible_inst clenv mv = (str "An incompatible instantiation has already been found for " ++ pr_id id) | _ -> - anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned") + anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned.") (* TODO: replace by clenv_unify (mkMeta mv) rhs ? *) let clenv_assign mv rhs clenv = let rhs_fls = mk_freelisted rhs in if Metaset.exists (mentions clenv mv) rhs_fls.freemetas then - error "clenv_assign: circularity in unification"; + user_err Pp.(str "clenv_assign: circularity in unification"); try if meta_defined clenv.evd mv then if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then @@ -174,7 +174,7 @@ let clenv_assign mv rhs clenv = let st = (Conv,TypeNotProcessed) in {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd} with Not_found -> - error "clenv_assign: undefined meta" + user_err Pp.(str "clenv_assign: undefined meta") @@ -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 ++ @@ -433,7 +433,7 @@ let explain_no_such_bound_variable evd id = | Cltyp (na, _) -> na | Clval (na, _, _) -> na in - if na != Anonymous then out_name na :: l else l + if na != Anonymous then Name.get_id na :: l else l in let mvl = List.fold_left fold [] (Evd.meta_list evd) in user_err ~hdr:"Evd.meta_with_name" @@ -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..b1fe128a2 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -39,11 +39,11 @@ let define_and_solve_constraints evk c env evd = pbs with | Success evd -> evd - | UnifFailure _ -> error "Instance does not satisfy the constraints." + | UnifFailure _ -> user_err Pp.(str "Instance does not satisfy the constraints.") let w_refine (evk,evi) (ltac_var,rawc) sigma = if Evd.is_defined sigma evk then - error "Instantiate called on already-defined evar"; + user_err Pp.(str "Instantiate called on already-defined evar"); let env = Evd.evar_filtered_env evi in let sigma',typed_c = let flags = { @@ -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/logic.ml b/proofs/logic.ml index 54345abd9..c329bdf4a 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -141,7 +141,7 @@ let occur_vars_in_decl env sigma hyps d = let reorder_context env sigma sign ord = let ords = List.fold_right Id.Set.add ord Id.Set.empty in if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then - error "Order list has duplicates"; + user_err Pp.(str "Order list has duplicates"); let rec step ord expected ctxt_head moved_hyps ctxt_tail = match ord with | [] -> List.rev ctxt_tail @ ctxt_head @@ -414,7 +414,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | _ -> if occur_meta sigma (EConstr.of_constr trm) then - anomaly (Pp.str "refiner called with a meta in non app/case subterm"); + anomaly (Pp.str "refiner called with a meta in non app/case subterm."); let (sigma, t'ty) = goal_type_of env sigma trm in let sigma = check_conv_leq_goal env sigma trm t'ty conclty in (goalacc,t'ty,sigma, trm) @@ -474,7 +474,7 @@ and mk_hdgoals sigma goal goalacc trm = | _ -> if !check && occur_meta sigma (EConstr.of_constr trm) then - anomaly (Pp.str "refine called with a dependent meta"); + anomaly (Pp.str "refine called with a dependent meta."); let (sigma, ty) = goal_type_of env sigma trm in goalacc, ty, sigma, trm @@ -502,7 +502,7 @@ and mk_casegoals sigma goal goalacc p c = let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in let ((ind, u), spec) = try Tacred.find_hnf_rectype env sigma ct - with Not_found -> anomaly (Pp.str "mk_casegoals") in + with Not_found -> anomaly (Pp.str "mk_casegoals.") in let indspec = ((ind, EConstr.EInstance.kind sigma u), spec) in let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in (acc'',lbrty,conclty,sigma,p',c') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 7e8ed31d1..3fb66d1b8 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); @@ -71,7 +71,7 @@ let get_universe_binders () = exception NoSuchGoal let _ = CErrors.register_handler begin function - | NoSuchGoal -> CErrors.error "No such goal." + | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") | _ -> raise CErrors.Unhandled end let get_nth_V82_goal i = @@ -87,12 +87,12 @@ let get_goal_context_gen i = let get_goal_context i = try get_goal_context_gen i - with Proof_global.NoCurrentProof -> CErrors.error "No focused proof." - | NoSuchGoal -> CErrors.error "No such goal." + with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.") + | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") let get_current_goal_context () = try get_goal_context_gen 1 - with Proof_global.NoCurrentProof -> CErrors.error "No focused proof." + with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.") | NoSuchGoal -> (* spiwack: returning empty evar_map, since if there is no goal, under focus, there is no accessible evar either *) @@ -113,7 +113,7 @@ let get_current_context () = let current_proof_statement () = match Proof_global.V82.get_current_initial_conclusions () with | (id,([concl],strength)) -> id,strength,concl - | _ -> CErrors.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 @@ -143,7 +143,7 @@ let solve ?with_end_tac gi info_lvl tac pr = in (p,status) with - Proof_global.NoCurrentProof -> CErrors.error "No focused proof" + Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof") let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) 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.ml b/proofs/proof.ml index b2103489a..2aa620c1d 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -66,14 +66,14 @@ exception FullyUnfocused let _ = CErrors.register_handler begin function | CannotUnfocusThisWay -> - CErrors.error "This proof is focused, but cannot be unfocused this way" + CErrors.user_err Pp.(str "This proof is focused, but cannot be unfocused this way") | NoSuchGoals (i,j) when Int.equal i j -> CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").") | NoSuchGoals (i,j) -> CErrors.user_err ~hdr:"Focus" Pp.( str"Not every goal in range ["++ int i ++ str","++int j++str"] exist." ) - | FullyUnfocused -> CErrors.error "The proof is not focused" + | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused") | _ -> raise CErrors.Unhandled end @@ -301,10 +301,10 @@ exception HasShelvedGoals exception HasGivenUpGoals exception HasUnresolvedEvar 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." + | UnfinishedProof -> CErrors.user_err Pp.(str "Some goals have not been solved.") + | HasShelvedGoals -> CErrors.user_err Pp.(str "Some goals have been left on the shelf.") + | HasGivenUpGoals -> CErrors.user_err Pp.(str "Some goals have been given up.") + | HasUnresolvedEvar -> CErrors.user_err Pp.(str "Some existential variables are uninstantiated.") | _ -> raise CErrors.Unhandled end @@ -420,9 +420,9 @@ module V82 = struct let evl = Evarutil.non_instantiated sigma in let evl = Evar.Map.bindings evl in if (n <= 0) then - CErrors.error "incorrect existential variable index" + CErrors.user_err Pp.(str "incorrect existential variable index") else if CList.length evl < n then - CErrors.error "not so many uninstantiated existential variables" + CErrors.user_err Pp.(str "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 5f4a7766f..5ec34a638 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -36,7 +36,7 @@ let proof_modes = Hashtbl.create 6 let find_proof_mode n = try Hashtbl.find proof_modes n with Not_found -> - CErrors.error (Format.sprintf "No proof mode named \"%s\"." n) + CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n)) let register_proof_mode ({name = n} as m) = Hashtbl.add proof_modes n (CEphemeron.create m) @@ -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 @@ -125,13 +124,13 @@ let push a l = l := a::!l; exception NoSuchProof let _ = CErrors.register_handler begin function - | NoSuchProof -> CErrors.error "No such proof." + | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.") | _ -> raise CErrors.Unhandled end exception NoCurrentProof let _ = CErrors.register_handler begin function - | NoCurrentProof -> CErrors.error "No focused proof (No proof-editing in progress)." + | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") | _ -> raise CErrors.Unhandled end @@ -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 @@ -301,7 +299,7 @@ let set_used_variables l = | [] -> raise NoCurrentProof | p :: rest -> if not (Option.is_empty p.section_vars) then - CErrors.error "Used section variables can be declared only once"; + CErrors.user_err Pp.(str "Used section variables can be declared only once"); pstates := { p with section_vars = Some ctx} :: rest; ctx, to_clear @@ -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"]; @@ -640,9 +637,9 @@ module Bullet = struct current_behavior := try Hashtbl.find behaviors n with Not_found -> - CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".") + CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\".")) end - } + }) let put p b = (!current_behavior).put p b @@ -690,15 +687,13 @@ 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 CErrors.error err_msg; + if i < 0 then CErrors.user_err Pp.(str err_msg); Vernacexpr.SelectNth i - with Failure _ -> CErrors.error err_msg + with Failure _ -> CErrors.user_err Pp.(str err_msg) 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 @@ -724,7 +719,7 @@ type state = pstate list let freeze ~marshallable = match marshallable with | `Yes -> - CErrors.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/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..383a6a523 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"]; @@ -195,7 +195,7 @@ let decl_red_expr s e = end let out_arg = function - | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") + | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.") | ArgArg x -> x let out_with_occurrences (occs,c) = 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} *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 259e96a27..91e6dc4ab 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -188,8 +188,6 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) (fun hypl -> List.subtract cmp hypl oldhyps) hyps in - let emacs_str s = - if !Flags.print_emacs then s else "" in let s = let frst = ref true in List.fold_left @@ -199,9 +197,9 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) "" lh)) "" newhyps in Feedback.msg_notice - (str (emacs_str "<infoH>") + (str "<infoH>" ++ (hov 0 (str s)) - ++ (str (emacs_str "</infoH>"))); + ++ (str "</infoH>")); tclIDTAC goal;; diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 97c5cda77..66d91c634 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -75,7 +75,7 @@ let pf_get_new_ids ids gls = (fun id acc -> (next_ident_away id (acc@avoid))::acc) ids [] -let pf_global gls id = EConstr.of_constr (Constrintern.construct_reference (pf_hyps gls) id) +let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id)) let pf_reduction_of_red_expr gls re c = let (redfun, _) = reduction_of_red_expr (pf_env gls) re in @@ -171,7 +171,7 @@ module New = struct (** We only check for the existence of an [id] in [hyps] *) let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in - EConstr.of_constr (Constrintern.construct_reference hyps id) + Constrintern.construct_reference hyps id let pf_env = Proofview.Goal.env let pf_concl = Proofview.Goal.concl diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index e6e60e27f..1172e55ac 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -100,7 +100,7 @@ val pr_glls : goal list sigma -> Pp.std_ppcmds (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig val pf_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a - val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr + val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> Globnames.global_reference (** FIXME: encapsulate the level in an existential type. *) val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a |