From 34f63d7d890921cce37f4d48f48cdb020f2ac988 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 26 Nov 2017 19:00:46 +0100 Subject: [proof] Embed evar_map in RefinerError exception. The exception needs to carry aroud a pair of `env, sigma` so printing is correct. This gets rid of a few global calls, and it is IMO the right thing to do. While we are at it, we incorporate some fixes to a couple of additional printing functions missing the `env, sigma` pair. --- API/API.mli | 2 +- plugins/ltac/rewrite.ml | 12 ++++++----- plugins/ltac/tacinterp.ml | 2 +- pretyping/classops.ml | 34 ++++++++++++++++--------------- pretyping/classops.mli | 2 +- printing/prettyp.ml | 12 +++++------ printing/prettyp.mli | 5 +++-- printing/printer.ml | 3 +-- printing/printer.mli | 3 +-- proofs/clenvtac.ml | 3 ++- proofs/logic.ml | 41 ++++++++++++++++++------------------- proofs/logic.mli | 6 +++--- proofs/tacmach.ml | 6 ++++-- tactics/class_tactics.ml | 17 ++++++++-------- tactics/eauto.ml | 15 +++++++------- tactics/equality.ml | 3 ++- tactics/hints.ml | 12 ++++------- tactics/tactics.ml | 51 ++++++++++++++++++++++++++++------------------- vernac/explainErr.ml | 3 +-- vernac/vernacentries.ml | 6 +++--- 20 files changed, 124 insertions(+), 114 deletions(-) diff --git a/API/API.mli b/API/API.mli index 3ed008ff5..c5a1743f7 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4801,7 +4801,7 @@ sig | IntroNeedsProduct | DoesNotOccurIn of Constr.t * Names.Id.t | NoSuchHyp of Names.Id.t - exception RefinerError of refiner_error + exception RefinerError of Environ.env * Evd.evar_map * refiner_error val catchable_exception : exn -> bool end diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c0060c5a7..1f2e5f7ac 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -2021,14 +2021,16 @@ let add_morphism glob binders m s n = (** Taken from original setoid_replace, to emulate the old rewrite semantics where lemmas are first instantiated and then rewrite proceeds. *) -let check_evar_map_of_evars_defs evd = +let check_evar_map_of_evars_defs env evd = let metas = Evd.meta_list evd in let check_freemetas_is_empty rebus = Evd.Metaset.iter (fun m -> - if Evd.meta_defined evd m then () else - raise - (Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m]))) + if Evd.meta_defined evd m then () + else begin + raise + (Logic.RefinerError (env, evd, Logic.UnresolvedBindings [Evd.meta_name evd m])) + end) in List.iter (fun (_,binding) -> @@ -2063,7 +2065,7 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env = let c1 = if l2r then nf c' else nf c1 and c2 = if l2r then nf c2 else nf c' and car = nf car and rel = nf rel in - check_evar_map_of_evars_defs sigma; + check_evar_map_of_evars_defs env sigma; let prf = nf prf in let prfty = nf (Retyping.get_type_of env sigma prf) in let sort = sort_of_rel env sigma but in diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index e0d7eca5f..9e47db1c3 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -420,7 +420,7 @@ let interp_hyp ist env sigma (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else Loc.raise ?loc (Logic.RefinerError (Logic.NoSuchHyp id)) + else Loc.raise ?loc (Logic.RefinerError (env, sigma, Logic.NoSuchHyp id)) let interp_hyp_list_as_list ist env sigma (loc,id as x) = try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index c36630f5d..6d5ee504e 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -322,16 +322,16 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; (* pretty-print functions are now in Pretty *) (* rajouter une coercion dans le graphe *) -let path_printer = ref (fun _ -> str "" - : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) +let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = + ref (fun _ _ _ -> str "") let install_path_printer f = path_printer := f -let print_path x = !path_printer x +let print_path env sigma x = !path_printer env sigma x -let message_ambig l = - (str"Ambiguous paths:" ++ spc () ++ - prlist_with_sep fnl (fun ijp -> print_path ijp) l) +let message_ambig env sigma l = + str"Ambiguous paths:" ++ spc () ++ + prlist_with_sep fnl (fun ijp -> print_path env sigma ijp) l (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) @@ -344,8 +344,8 @@ let different_class_params i = | CL_IND i -> Global.is_polymorphic (IndRef i) | CL_CONST c -> Global.is_polymorphic (ConstRef c) | _ -> false - -let add_coercion_in_graph (ic,source,target) = + +let add_coercion_in_graph env sigma (ic,source,target) = let old_inheritance_graph = !inheritance_graph in let ambig_paths = (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in @@ -387,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) = end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in if is_ambig && not !Flags.quiet then - Feedback.msg_info (message_ambig !ambig_paths) + Feedback.msg_info (message_ambig env sigma !ambig_paths) type coercion = { coercion_type : coe_typ; @@ -433,13 +433,13 @@ let _ = optread = (fun () -> !automatically_import_coercions); optwrite = (:=) automatically_import_coercions } -let cache_coercion (_, c) = +let cache_coercion env sigma (_, c) = let () = add_class c.coercion_source in let () = add_class c.coercion_target in let is, _ = class_info c.coercion_source in let it, _ = class_info c.coercion_target in - let value, ctx = Universes.fresh_global_instance (Global.env()) c.coercion_type in - let typ = Retyping.get_type_of (Global.env ()) Evd.empty (EConstr.of_constr value) in + let value, ctx = Universes.fresh_global_instance env c.coercion_type in + let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in let typ = EConstr.Unsafe.to_constr typ in let xf = { coe_value = value; @@ -450,15 +450,15 @@ let cache_coercion (_, c) = coe_is_projection = c.coercion_is_proj; coe_param = c.coercion_params } in let () = add_new_coercion c.coercion_type xf in - add_coercion_in_graph (xf,is,it) + add_coercion_in_graph env sigma (xf,is,it) let load_coercion _ o = if !automatically_import_coercions then - cache_coercion o + cache_coercion (Global.env ()) Evd.empty o let open_coercion i o = if Int.equal i 1 && not !automatically_import_coercions then - cache_coercion o + cache_coercion (Global.env ()) Evd.empty o let subst_coercion (subst, c) = let coe = subst_coe_typ subst c.coercion_type in @@ -497,7 +497,9 @@ let inCoercion : coercion -> obj = declare_object {(default_object "COERCION") with open_function = open_coercion; load_function = load_coercion; - cache_function = cache_coercion; + cache_function = (fun objn -> + let env = Global.env () in cache_coercion env Evd.empty objn + ); subst_function = subst_coercion; classify_function = classify_coercion; discharge_function = discharge_coercion } diff --git a/pretyping/classops.mli b/pretyping/classops.mli index b41d0efac..47b41f17b 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -96,7 +96,7 @@ val lookup_pattern_path_between : (**/**) (* Crade *) val install_path_printer : - ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit + (env -> evar_map -> (cl_index * cl_index) * inheritance_path -> Pp.t) -> unit (**/**) (** {6 This is for printing purpose } *) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 1eb2c31c8..647111bbe 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -903,18 +903,16 @@ let print_class i = let cl,_ = class_info_from_index i in pr_class cl -let print_path ((i,j),p) = - let sigma, env = Pfedit.get_current_context () in +let print_path env sigma ((i,j),p) = hov 2 ( str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++ str"] : ") ++ print_class i ++ str" >-> " ++ print_class j -(* XXX: This is suspicious!!! *) let _ = Classops.install_path_printer print_path -let print_graph () = - prlist_with_sep fnl print_path (inheritance_graph()) +let print_graph env sigma = + prlist_with_sep fnl (print_path env sigma) (inheritance_graph()) let print_classes () = pr_sequence pr_class (classes()) @@ -929,7 +927,7 @@ let index_of_class cl = user_err ~hdr:"index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") -let print_path_between cls clt = +let print_path_between env sigma cls clt = let i = index_of_class cls in let j = index_of_class clt in let p = @@ -940,7 +938,7 @@ let print_path_between cls clt = (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in - print_path ((i,j),p) + print_path env sigma ((i,j),p) let print_canonical_projections env sigma = prlist_with_sep fnl diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 8f3a6ddc4..fd7f1f92b 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -12,6 +12,7 @@ open Reductionops open Libnames open Globnames open Misctypes +open Evd (** A Pretty-Printer for the Calculus of Inductive Constructions. *) @@ -39,10 +40,10 @@ val print_about : env -> Evd.evar_map -> reference or_by_notation -> val print_impargs : reference or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) -val print_graph : unit -> Pp.t +val print_graph : env -> evar_map -> Pp.t val print_classes : unit -> Pp.t val print_coercions : env -> Evd.evar_map -> Pp.t -val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t +val print_path_between : env -> evar_map -> Classops.cl_typ -> Classops.cl_typ -> Pp.t val print_canonical_projections : env -> Evd.evar_map -> Pp.t (** Pretty-printing functions for type classes and instances *) diff --git a/printing/printer.ml b/printing/printer.ml index 6a0597860..a63004ceb 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -905,7 +905,7 @@ end module ContextObjectSet = Set.Make (OrderedContextObject) module ContextObjectMap = Map.Make (OrderedContextObject) -let pr_assumptionset env s = +let pr_assumptionset env sigma s = if ContextObjectMap.is_empty s && engagement env = PredicativeSet then str "Closed under the global context" @@ -921,7 +921,6 @@ let pr_assumptionset env s = with e when CErrors.noncritical e -> mt () in let safe_pr_ltype_relctx (rctx, typ) = - let sigma, env = Pfedit.get_current_context () in let env = Environ.push_rel_context rctx env in try str " " ++ pr_ltype_env env sigma typ with e when CErrors.noncritical e -> mt () diff --git a/printing/printer.mli b/printing/printer.mli index 36ca1bdcc..804014745 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -217,8 +217,7 @@ module ContextObjectSet : Set.S with type elt = context_object module ContextObjectMap : CMap.ExtS with type key = context_object and module Set := ContextObjectSet -val pr_assumptionset : - env -> types ContextObjectMap.t -> Pp.t +val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 4a92c3856..8bd5d98cb 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -54,9 +54,10 @@ let clenv_value_cast_meta clenv = let clenv_pose_dependent_evars with_evars clenv = let dep_mvs = clenv_dependent clenv in + let env, sigma = clenv.env, clenv.evd in if not (List.is_empty dep_mvs) && not with_evars then raise - (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); + (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); clenv_pose_metas_as_evars clenv dep_mvs (** Use our own fast path, more informative than from Typeclasses *) diff --git a/proofs/logic.ml b/proofs/logic.ml index a9ad606a0..1d86a0909 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -40,7 +40,7 @@ type refiner_error = | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t -exception RefinerError of refiner_error +exception RefinerError of Environ.env * Evd.evar_map * refiner_error open Pretype_errors @@ -69,7 +69,7 @@ let catchable_exception = function | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e | _ -> false -let error_no_such_hypothesis id = raise (RefinerError (NoSuchHyp id)) +let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id)) (* Tells if the refiner should check that the submitted rules do not produce invalid subgoals *) @@ -78,10 +78,10 @@ let with_check = Flags.with_option check (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and returns [tail::(f head (id,_,_) (rev tail))] *) -let apply_to_hyp check sign id f = +let apply_to_hyp env sigma check sign id f = try apply_to_hyp sign id f with Hyp_not_found -> - if check then error_no_such_hypothesis id + if check then error_no_such_hypothesis env sigma id else sign let check_typability env sigma c = @@ -147,7 +147,7 @@ let reorder_context env sigma sign ord = step ord' expected ctxt_head mh (d::ctxt_tail) | _ -> (match ctxt_head with - | [] -> error_no_such_hypothesis (List.hd ord) + | [] -> error_no_such_hypothesis env sigma (List.hd ord) | d :: ctxt -> let x = NamedDecl.get_id d in if Id.Set.mem x expected then @@ -190,9 +190,9 @@ let move_location_eq m1 m2 = match m1, m2 with | MoveFirst, MoveFirst -> true | _ -> false -let split_sign hfrom hto l = +let split_sign env sigma hfrom hto l = let rec splitrec left toleft = function - | [] -> error_no_such_hypothesis hfrom + | [] -> error_no_such_hypothesis env sigma hfrom | d :: right -> let hyp = NamedDecl.get_id d in if Id.equal hyp hfrom then @@ -222,7 +222,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto = let rec moverec first middle = function | [] -> if match hto with MoveFirst | MoveLast -> false | _ -> true then - error_no_such_hypothesis (hyp_of_move_location hto); + error_no_such_hypothesis env sigma (hyp_of_move_location hto); List.rev first @ List.rev middle | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) -> List.rev first @ List.rev middle @ right @@ -258,10 +258,10 @@ let move_hyp sigma toleft (left,declfrom,right) hto = List.fold_left (fun sign d -> push_named_context_val d sign) right left -let move_hyp_in_named_context sigma hfrom hto sign = +let move_hyp_in_named_context env sigma hfrom hto sign = let open EConstr in let (left,right,declfrom,toleft) = - split_sign hfrom hto (named_context_of_val sign) in + split_sign env sigma hfrom hto (named_context_of_val sign) in move_hyp sigma toleft (left,declfrom,right) hto let insert_decl_in_named_context sigma decl hto sign = @@ -293,15 +293,15 @@ let collect_meta_variables c = in List.rev (collrec false [] c) -let check_meta_variables c = +let check_meta_variables env sigma c = if not (List.distinct_f Int.compare (collect_meta_variables c)) then - raise (RefinerError (NonLinearProof c)) + raise (RefinerError (env, sigma, NonLinearProof c)) let check_conv_leq_goal env sigma arg ty conclty = if !check then let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in if b then evm - else raise (RefinerError (BadType (arg,ty,conclty))) + else raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) else sigma exception Stop of EConstr.t list @@ -336,7 +336,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | Meta _ -> let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in if !check && occur_meta sigma conclty then - raise (RefinerError (MetaInType conclty)); + raise (RefinerError (env, sigma, MetaInType conclty)); let (gl,ev,sigma) = mk_goal hyps conclty in let ev = EConstr.Unsafe.to_constr ev in let conclty = EConstr.Unsafe.to_constr conclty in @@ -477,7 +477,9 @@ and mk_arggoals sigma goal goalacc funty allargs = | Prod (_, c1, b) -> let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in (acc, subst1 harg b, sigma), arg - | _ -> raise (RefinerError (CannotApply (t, harg))) + | _ -> + let env = Goal.V82.env sigma goal in + raise (RefinerError (env,sigma,CannotApply (t, harg))) in Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs @@ -497,10 +499,10 @@ and mk_casegoals sigma goal goalacc p c = let convert_hyp check sign sigma d = let id = NamedDecl.get_id d in let b = NamedDecl.get_value d in - let env = Global.env() in + let env = Global.env () in let reorder = ref [] in let sign' = - apply_to_hyp check sign id + apply_to_hyp env sigma check sign id (fun _ d' _ -> let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in let env = Global.env_of_context sign in @@ -514,19 +516,18 @@ let convert_hyp check sign sigma d = map_named_decl EConstr.Unsafe.to_constr d) in reorder_val_context env sigma sign' !reorder - - (************************************************************************) (************************************************************************) (* Primitive tactics are handled here *) let prim_refiner r sigma goal = + let env = Goal.V82.env sigma goal in let cl = Goal.V82.concl sigma goal in match r with (* Logical rules *) | Refine c -> let cl = EConstr.Unsafe.to_constr cl in - check_meta_variables c; + check_meta_variables env sigma c; let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in let sgl = List.rev sgl in let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in diff --git a/proofs/logic.mli b/proofs/logic.mli index 7df7fd66b..afd1ecf70 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -50,16 +50,16 @@ type refiner_error = | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t -exception RefinerError of refiner_error +exception RefinerError of Environ.env * evar_map * refiner_error -val error_no_such_hypothesis : Id.t -> 'a +val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> EConstr.named_declaration -> Environ.named_context_val -val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> +val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> Environ.named_context_val -> Environ.named_context_val val insert_decl_in_named_context : Evd.evar_map -> diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index cab8d7b52..d41541251 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -55,10 +55,11 @@ let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id let pf_last_hyp gl = List.hd (pf_hyps gl) let pf_get_hyp gls id = + let env, sigma = pf_env gls, project gls in try Context.Named.lookup id (pf_hyps gls) with Not_found -> - raise (RefinerError (NoSuchHyp id)) + raise (RefinerError (env, sigma, NoSuchHyp id)) let pf_get_hyp_typ gls id = id |> pf_get_hyp gls |> NamedDecl.get_type @@ -182,9 +183,10 @@ module New = struct let pf_get_hyp id gl = let hyps = Proofview.Goal.env gl in + let sigma = project gl in let sign = try EConstr.lookup_named id hyps - with Not_found -> raise (RefinerError (NoSuchHyp id)) + with Not_found -> raise (RefinerError (hyps, sigma, NoSuchHyp id)) in sign diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index cee6d4bea..9e4d132d4 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -376,7 +376,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars = Proofview.Goal.enter begin fun gl -> let tacs = e_trivial_resolve db_list local_db secvars only_classes - (project gl) (pf_concl gl) in + (pf_env gl) (project gl) (pf_concl gl) in tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs) end in @@ -386,7 +386,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars = in tclFIRST (List.map tclCOMPLETE tacl) -and e_my_find_search db_list local_db secvars hdc complete only_classes sigma concl = +and e_my_find_search db_list local_db secvars hdc complete only_classes env sigma concl = let open Proofview.Notations in let prods, concl = EConstr.decompose_prod_assum sigma concl in let nprods = List.length prods in @@ -464,7 +464,6 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co in let tac = run_hint t tac in let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in - let _, env = Pfedit.get_current_context () in let pp = match p with | Some pat when get_typeclasses_filtered_unification () -> @@ -476,16 +475,16 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp)) in List.map tac_of_hint hintl -and e_trivial_resolve db_list local_db secvars only_classes sigma concl = +and e_trivial_resolve db_list local_db secvars only_classes env sigma concl = let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in try - e_my_find_search db_list local_db secvars hd true only_classes sigma concl + e_my_find_search db_list local_db secvars hd true only_classes env sigma concl with Not_found -> [] -let e_possible_resolve db_list local_db secvars only_classes sigma concl = +let e_possible_resolve db_list local_db secvars only_classes env sigma concl = let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in try - e_my_find_search db_list local_db secvars hd false only_classes sigma concl + e_my_find_search db_list local_db secvars hd false only_classes env sigma concl with Not_found -> [] let cut_of_hints h = @@ -719,7 +718,7 @@ module V85 = struct let concl = Goal.V82.concl s gl in let tacgl = {it = gl; sigma = s;} in let secvars = secvars_of_hyps (Environ.named_context_of_val (Goal.V82.hyps s gl)) in - let poss = e_possible_resolve hints info.hints secvars info.only_classes s concl in + let poss = e_possible_resolve hints info.hints secvars info.only_classes env s concl in let unique = is_unique env s concl in let rec aux i foundone = function | (tac, _, extern, name, pp) :: tl -> @@ -1072,7 +1071,7 @@ module Search = struct else str" without backtracking")); let secvars = compute_secvars gl in let poss = - e_possible_resolve hints info.search_hints secvars info.search_only_classes sigma concl in + e_possible_resolve hints info.search_hints secvars info.search_only_classes env sigma concl in (* If no goal depends on the solution of this one or the instances are irrelevant/assumed to be unique, then we don't need to backtrack, as long as no evar appears in the goal diff --git a/tactics/eauto.ml b/tactics/eauto.ml index f5c6ab879..d2e014e55 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -148,12 +148,12 @@ let rec e_trivial_fail_db db_list local_db = let tacl = registered_e_assumption :: (Tacticals.New.tclTHEN Tactics.intro next) :: - (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl))) + (List.map fst (e_trivial_resolve (Tacmach.New.pf_env gl) (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl))) in Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl) end -and e_my_find_search sigma db_list local_db secvars hdc concl = +and e_my_find_search env sigma db_list local_db secvars hdc concl = let hint_of_db = hintmap_of sigma secvars hdc concl in let hintl = List.map_append (fun db -> @@ -178,20 +178,19 @@ and e_my_find_search sigma db_list local_db secvars hdc concl = | Extern tacast -> conclPattern concl p tacast in let tac = run_hint t tac in - let sigma, env = Pfedit.get_current_context () in (tac, lazy (pr_hint env sigma t))) in List.map tac_of_hint hintl -and e_trivial_resolve sigma db_list local_db secvars gl = +and e_trivial_resolve env sigma db_list local_db secvars gl = let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in - try priority (e_my_find_search sigma db_list local_db secvars hd gl) + try priority (e_my_find_search env sigma db_list local_db secvars hd gl) with Not_found -> [] -let e_possible_resolve sigma db_list local_db secvars gl = +let e_possible_resolve env sigma db_list local_db secvars gl = let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) - (e_my_find_search sigma db_list local_db secvars hd gl) + (e_my_find_search env sigma db_list local_db secvars hd gl) with Not_found -> [] let find_first_goal gls = @@ -291,7 +290,7 @@ module SearchProblem = struct let l = let concl = Reductionops.nf_evar (project g) (pf_concl g) in filter_tactics s.tacres - (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl) + (e_possible_resolve (pf_env g) (project g) s.dblist (List.hd s.localdb) secvars concl) in List.map (fun (lgls, cost, pp) -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 0d6263246..22073d39b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1436,8 +1436,9 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = (tac (clenv_value eq_clause)) let get_previous_hyp_position id gl = + let env, sigma = Proofview.Goal.(env gl, sigma gl) in let rec aux dest = function - | [] -> raise (RefinerError (NoSuchHyp id)) + | [] -> raise (RefinerError (env, sigma, NoSuchHyp id)) | d :: right -> let hyp = Context.Named.Declaration.get_id d in if Id.equal hyp id then dest else aux (MoveAfter hyp) right diff --git a/tactics/hints.ml b/tactics/hints.ml index 70e84013b..7f9b5ef34 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1400,15 +1400,10 @@ let pr_hint env sigma h = match h.obj with | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c) | Res_pf_THEN_trivial_fail (c, _) -> (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial") - | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) + | Unfold_nth c -> + str"unfold " ++ pr_evaluable_reference c | Extern tac -> - let env = - try - let (_, env) = Pfedit.get_current_goal_context () in - env - with e when CErrors.noncritical e -> Global.env () - in - (str "(*external*) " ++ Pputils.pr_glb_generic env tac) + str "(*external*) " ++ Pputils.pr_glb_generic env tac let pr_id_hint env sigma (id, v) = let pr_pat p = str", pattern " ++ pr_lconstr_pattern_env env sigma p in @@ -1507,6 +1502,7 @@ let pr_hint_db_env env sigma db = hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++ content +(* Deprecated in the mli *) let pr_hint_db db = let sigma, env = Pfedit.get_current_context () in pr_hint_db_env env sigma db diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e072bd95f..6aa052d32 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -187,7 +187,7 @@ let introduction ?(check=true) id = match EConstr.kind sigma concl with | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b - | _ -> raise (RefinerError IntroNeedsProduct) + | _ -> raise (RefinerError (env, sigma, IntroNeedsProduct)) end let refine = Tacmach.refine @@ -319,7 +319,7 @@ let move_hyp id dest = let ty = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in let sign = named_context_val env in - let sign' = move_hyp_in_named_context sigma id dest sign in + let sign' = move_hyp_in_named_context env sigma id dest sign in let env = reset_with_named_context sign' env in Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar env sigma ~principal:true ~store ty @@ -348,13 +348,15 @@ let rename_hyp repl = let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in (** Check that we do not mess variables *) let fold accu decl = Id.Set.add (NamedDecl.get_id decl) accu in let vars = List.fold_left fold Id.Set.empty hyps in let () = if not (Id.Set.subset src vars) then let hyp = Id.Set.choose (Id.Set.diff src vars) in - raise (RefinerError (NoSuchHyp hyp)) + raise (RefinerError (env, sigma, NoSuchHyp hyp)) in let mods = Id.Set.diff vars src in let () = @@ -442,9 +444,9 @@ let find_name mayrepl decl naming gl = match naming with (* Computing position of hypotheses for replacing *) (**************************************************************) -let get_next_hyp_position id = +let get_next_hyp_position env sigma id = let rec aux = function - | [] -> error_no_such_hypothesis id + | [] -> error_no_such_hypothesis env sigma id | decl :: right -> if Id.equal (NamedDecl.get_id decl) id then match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveFirst @@ -453,9 +455,9 @@ let get_next_hyp_position id = in aux -let get_previous_hyp_position id = +let get_previous_hyp_position env sigma id = let rec aux dest = function - | [] -> error_no_such_hypothesis id + | [] -> error_no_such_hypothesis env sigma id | decl :: right -> let hyp = NamedDecl.get_id decl in if Id.equal hyp id then dest else aux (MoveAfter hyp) right @@ -483,7 +485,7 @@ let internal_cut_gen ?(check=true) dir replace id t = let sign = named_context_val env in let sign',t,concl,sigma = if replace then - let nexthyp = get_next_hyp_position id (named_context_of_val sign) in + let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in sign',t,concl,sigma @@ -1000,6 +1002,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in + let env = Tacmach.New.pf_env gl in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in match EConstr.kind sigma concl with | Prod (name,t,u) when not dep_flag || not (noccurn sigma 1 u) -> @@ -1009,7 +1012,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac | _ -> - begin if not force_flag then Proofview.tclZERO (RefinerError IntroNeedsProduct) + begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct)) (* Note: red_in_concl includes betaiotazeta and this was like *) (* this since at least V6.3 (a pity *) (* that intro do betaiotazeta only when reduction is needed; and *) @@ -1020,7 +1023,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = (Tacticals.New.tclTHEN hnf_in_concl (intro_then_gen name_flag move_flag false dep_flag tac)) begin function (e, info) -> match e with - | RefinerError IntroNeedsProduct -> + | RefinerError (env, sigma, IntroNeedsProduct) -> Tacticals.New.tclZEROMSG (str "No product even after head-reduction.") | e -> Proofview.tclZERO ~info e end @@ -1059,7 +1062,7 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = (fun id -> aux (n+1) (id::ids)) end begin function (e, info) -> match e with - | RefinerError IntroNeedsProduct -> + | RefinerError (env, sigma, IntroNeedsProduct) -> tac ids | e -> Proofview.tclZERO ~info e end @@ -1070,8 +1073,9 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = let intro_replacing id = Proofview.Goal.enter begin fun gl -> + let env, sigma = Proofview.Goal.(env gl, sigma gl) in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let next_hyp = get_next_hyp_position id hyps in + let next_hyp = get_next_hyp_position env sigma id hyps in Tacticals.New.tclTHENLIST [ clear_for_replacing [id]; introduction id; @@ -1090,8 +1094,9 @@ let intro_replacing id = let intros_possibly_replacing ids = let suboptimal = true in Proofview.Goal.enter begin fun gl -> + let env, sigma = Proofview.Goal.(env gl, sigma gl) in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in + let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in Tacticals.New.tclTHEN (Tacticals.New.tclMAP (fun id -> Tacticals.New.tclTRY (clear_for_replacing [id])) @@ -1105,7 +1110,8 @@ let intros_possibly_replacing ids = let intros_replacing ids = Proofview.Goal.enter begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in + let env, sigma = Proofview.Goal.(env gl, sigma gl) in + let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in Tacticals.New.tclTHEN (clear_for_replacing ids) (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl) @@ -2633,8 +2639,10 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars Proofview.Goal.enter begin fun gl -> let destopt = if with_evars then MoveLast (* evars would depend on the whole context *) - else - get_previous_hyp_position id (Proofview.Goal.hyps (Proofview.Goal.assume gl)) in + else ( + let env, sigma = Proofview.Goal.(env gl, sigma gl) in + get_previous_hyp_position env sigma id (Proofview.Goal.hyps (Proofview.Goal.assume gl)) + ) in let naming,ipat_tac = prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in let lemmas_target, last_lemma_target = @@ -4448,8 +4456,11 @@ let check_enough_applied env sigma elim = check_expected_type env sigma elimc elimt let guard_no_unifiable = Proofview.guard_no_unifiable >>= function -| None -> Proofview.tclUNIT () -| Some l -> Proofview.tclZERO (RefinerError (UnresolvedBindings l)) + | None -> Proofview.tclUNIT () + | Some l -> + Proofview.tclENV >>= function env -> + Proofview.tclEVARMAP >>= function sigma -> + Proofview.tclZERO (RefinerError (env, sigma, UnresolvedBindings l)) let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim id ((pending,(c0,lbind)),(eqname,names)) t0 inhyps cls tac = @@ -4648,7 +4659,7 @@ let induction_destruct isrec with_evars (lc,elim) = (Tacticals.New.tclMAP (fun (a,b,cl) -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in + let sigma = Tacmach.New.project gl in onOpenInductionArg env sigma (fun clear_flag a -> induction_gen clear_flag false with_evars None (a,b) cl) a end) l) @@ -4673,7 +4684,7 @@ let induction_destruct isrec with_evars (lc,elim) = end let induction ev clr c l e = - induction_gen clr true ev e + induction_gen clr true ev e ((Evd.empty,(c,NoBindings)),(None,l)) None let destruct ev clr c l e = diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 3a8e8fb43..d328ad0cf 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -75,8 +75,7 @@ let process_vernac_interp_error exn = match fst exn with wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e) | Tacred.ReductionTacticError e -> wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) - | Logic.RefinerError e -> - let sigma, env = Pfedit.get_current_context () in + | Logic.RefinerError (env, sigma, e) -> wrap_vernac_error exn (Himsg.explain_refiner_error env sigma e) | Nametab.GlobalizationError q -> wrap_vernac_error exn diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 63768d9b8..16a212511 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1656,13 +1656,13 @@ let vernac_print ~atts env sigma = | PrintMLModules -> msg_notice (Mltop.print_ml_modules ()) | PrintDebugGC -> msg_notice (Mltop.print_gc ()) | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl) - | PrintGraph -> msg_notice (Prettyp.print_graph()) + | PrintGraph -> msg_notice (Prettyp.print_graph env sigma) | PrintClasses -> msg_notice (Prettyp.print_classes()) | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses()) | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c)) | PrintCoercions -> msg_notice (Prettyp.print_coercions env sigma) | PrintCoercionPaths (cls,clt) -> - msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) + msg_notice (Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt)) | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections env sigma) | PrintUniverses (b, dst) -> let univ = Global.universes () in @@ -1696,7 +1696,7 @@ let vernac_print ~atts env sigma = let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in let nassums = Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in - msg_notice (Printer.pr_assumptionset (Global.env ()) nassums) + msg_notice (Printer.pr_assumptionset env sigma nassums) | PrintStrategy r -> print_strategy r let global_module r = -- cgit v1.2.3