diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 30 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 12 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 24 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 10 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 60 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 4 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 18 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 16 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 8 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 46 |
11 files changed, 122 insertions, 108 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 52094cf085..b0ffc775b5 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1,5 +1,5 @@ open Printer -open Errors +open CErrors open Util open Term open Vars @@ -27,7 +27,7 @@ let observe strm = let do_observe_tac s tac g = try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v with e -> - let e = Cerrors.process_vernac_interp_error e in + let e = ExplainErr.process_vernac_interp_error e in let goal = begin try (Printer.pr_goal g) with _ -> assert false end in msg_debug (str "observation "++ s++str " raised exception " ++ Errors.print e ++ str " on goal " ++ goal ); @@ -52,7 +52,7 @@ let rec print_debug_queue e = let _ = match e with | Some e -> - Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) + Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal)) | None -> begin Feedback.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal); @@ -74,9 +74,9 @@ let do_observe_tac s tac g = ignore(Stack.pop debug_queue); v with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in if not (Stack.is_empty debug_queue) - then print_debug_queue (Some (fst (Cerrors.process_vernac_interp_error reraise))); + then print_debug_queue (Some (fst (ExplainErr.process_vernac_interp_error reraise))); iraise reraise let observe_tac_stream s tac g = @@ -141,7 +141,7 @@ let is_trivial_eq t = eq_constr t1 t2 && eq_constr a1 a2 | _ -> false end - with e when Errors.noncritical e -> false + with e when CErrors.noncritical e -> false in (* observe (str "is_trivial_eq " ++ Printer.pr_lconstr t ++ (if res then str " true" else str " false")); *) res @@ -167,7 +167,7 @@ let is_incompatible_eq t = (eq_constr u1 u2 && incompatible_constructor_terms t1 t2) | _ -> false - with e when Errors.noncritical e -> false + with e when CErrors.noncritical e -> false in if res then observe (str "is_incompatible_eq " ++ Printer.pr_lconstr t); res @@ -223,8 +223,8 @@ let isAppConstruct ?(env=Global.env ()) t = let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) let clos_norm_flags flgs env sigma t = - Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in - clos_norm_flags Closure.betaiotazeta Environ.empty_env Evd.empty + CClosure.norm_val (CClosure.create_clos_infos flgs env) (CClosure.inject (Reductionops.nf_evar sigma t)) in + clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty @@ -254,7 +254,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = then (jmeq_refl (),(args.(1),args.(0)),(args.(3),args.(2)),args.(0)) else nochange "not an equality" - with e when Errors.noncritical e -> nochange "not an equality" + with e when CErrors.noncritical e -> nochange "not an equality" in if not ((closed0 (fst t1)) && (closed0 (snd t1)))then nochange "not a closed lhs"; let rec compute_substitution sub t1 t2 = @@ -281,7 +281,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = List.fold_left2 compute_substitution sub args1 args2 end else - if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_betadeltaiota env t1) t2) "cannot solve (diff)" + if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_all env t1) t2) "cannot solve (diff)" in let sub = compute_substitution Int.Map.empty (snd t1) (snd t2) in let sub = compute_substitution sub (fst t1) (fst t2) in @@ -625,8 +625,8 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = let my_orelse tac1 tac2 g = try tac1 g - with e when Errors.noncritical e -> -(* observe (str "using snd tac since : " ++ Errors.print e); *) + with e when CErrors.noncritical e -> +(* observe (str "using snd tac since : " ++ CErrors.print e); *) tac2 g let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = @@ -1025,7 +1025,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a {finfos with equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with ConstRef c -> c - | _ -> Errors.anomaly (Pp.str "Not a constant") + | _ -> CErrors.anomaly (Pp.str "Not a constant") ) } | _ -> () @@ -1085,7 +1085,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam match Global.body_of_constant const with | Some body -> Tacred.cbv_norm_flags - (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) (Global.env ()) (Evd.empty) body diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 5b4fb25955..5e72b8672a 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -1,5 +1,5 @@ open Printer -open Errors +open CErrors open Util open Term open Vars @@ -358,7 +358,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) Don't forget to close the goal if an error is raised !!!! *) save false new_princ_name entry g_kind hook - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> begin begin try @@ -370,7 +370,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) then Pfedit.delete_current_proof () else () else () - with e when Errors.noncritical e -> () + with e when CErrors.noncritical e -> () end; raise (Defining_principle e) end @@ -400,7 +400,7 @@ let get_funs_constant mp dp = match Global.body_of_constant const with | Some body -> let body = Tacred.cbv_norm_flags - (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) (Global.env ()) (Evd.from_env (Global.env ())) body @@ -510,7 +510,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con 0 (prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs))) (fun _ _ _ -> ()) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> begin begin try @@ -522,7 +522,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con then Pfedit.delete_current_proof () else () else () - with e when Errors.noncritical e -> () + with e when CErrors.noncritical e -> () end; raise (Defining_principle e) end diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 893baad8c9..42e4903155 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -90,7 +90,7 @@ let pr_intro_as_pat _prc _ _ pat = let out_disjunctive = function | loc, IntroAction (IntroOrAndPattern l) -> (loc,l) - | _ -> Errors.error "Disjunctive or conjunctive intro pattern expected." + | _ -> CErrors.error "Disjunctive or conjunctive intro pattern expected." ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat | [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] @@ -195,18 +195,16 @@ END let warning_error names e = - let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in + let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> - Feedback.msg_warning - (str "Cannot define graph(s) for " ++ - h 1 (pr_enum Libnames.pr_reference names) ++ - if do_observe () then (spc () ++ Errors.print e) else mt ()) + let names = pr_enum Libnames.pr_reference names in + let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in + warn_cannot_define_graph (names,error) | Defining_principle e -> - Feedback.msg_warning - (str "Cannot define principle(s) for "++ - h 1 (pr_enum Libnames.pr_reference names) ++ - if do_observe () then Errors.print e else mt ()) + let names = pr_enum Libnames.pr_reference names in + let error = if do_observe () then CErrors.print e else mt () in + warn_cannot_define_principle (names,error) | _ -> raise e @@ -229,15 +227,15 @@ VERNAC COMMAND EXTEND NewFunctionalScheme ; try Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> - Errors.error ("Cannot generate induction principle(s)") - | e when Errors.noncritical e -> + CErrors.error ("Cannot generate induction principle(s)") + | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e end | _ -> assert false (* we can only have non empty list *) end - | e when Errors.noncritical e -> + | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e end diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index c424fe1226..52179ae508 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -7,7 +7,7 @@ open Glob_term open Glob_ops open Globnames open Indfun_common -open Errors +open CErrors open Util open Glob_termops open Misctypes @@ -921,7 +921,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = observe (str "computing new type for eq : " ++ pr_glob_constr rt); let t' = try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*) - with e when Errors.noncritical e -> raise Continue + with e when CErrors.noncritical e -> raise Continue in let is_in_b = is_free_in id b in let _keep_eq = @@ -1223,7 +1223,7 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) l := param::!l ) rels_params.(0) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> () in List.rev !l @@ -1460,7 +1460,7 @@ let do_build_inductive str "while trying to define"++ spc () ++ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ - Errors.print reraise + CErrors.print reraise in observe msg; raise reraise @@ -1476,7 +1476,7 @@ let build_inductive evd funconstants funsargs returned_types rtl = do_build_inductive evd funconstants funsargs returned_types rtl; Detyping.print_universes := pu; Constrextern.print_universes := cu - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> Detyping.print_universes := pu; Constrextern.print_universes := cu; raise (Building_graph e) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 291f835ee7..01e5ef7fba 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,6 +1,6 @@ open Pp open Glob_term -open Errors +open CErrors open Util open Names open Decl_kinds diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 0cacb003d8..18817f504c 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,5 +1,5 @@ open Context.Rel.Declaration -open Errors +open CErrors open Util open Names open Term @@ -132,6 +132,7 @@ let rec abstract_glob_constr c = function | Constrexpr.LocalRawAssum (idl,k,t)::bl -> List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl (abstract_glob_constr c bl) + | Constrexpr.LocalPattern _::bl -> assert false let interp_casted_constr_with_implicits env sigma impls c = Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls @@ -215,6 +216,7 @@ let rec local_binders_length = function | [] -> 0 | Constrexpr.LocalRawDef _::bl -> 1 + local_binders_length bl | Constrexpr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl + | Constrexpr.LocalPattern _::bl -> assert false let prepare_body ((name,_,args,types,_),_) rt = let n = local_binders_length args in @@ -223,7 +225,12 @@ let prepare_body ((name,_,args,types,_),_) rt = (fun_args,rt') let process_vernac_interp_error e = - fst (Cerrors.process_vernac_interp_error (e, Exninfo.null)) + fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null)) + +let warn_funind_cannot_build_inversion = + CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind" + (fun e' -> strbrk "Cannot build inversion information" ++ + if do_observe () then (fnl() ++ CErrors.print e') else mt ()) let derive_inversion fix_names = try @@ -265,16 +272,22 @@ let derive_inversion fix_names = functional_induction fix_names_as_constant lind; - with e when Errors.noncritical e -> - let e' = process_vernac_interp_error e in - Feedback.msg_warning - (str "Cannot build inversion information" ++ - if do_observe () then (fnl() ++ Errors.print e') else mt ()) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> let e' = process_vernac_interp_error e in - Feedback.msg_warning - (str "Cannot build inversion information (early)" ++ - if do_observe () then (fnl() ++ Errors.print e') else mt ()) + warn_funind_cannot_build_inversion e' + with e when CErrors.noncritical e -> + let e' = process_vernac_interp_error e in + warn_funind_cannot_build_inversion e' + +let warn_cannot_define_graph = + CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind" + (fun (names,error) -> strbrk "Cannot define graph(s) for " ++ + h 1 names ++ error) + +let warn_cannot_define_principle = + CWarnings.create ~name:"funind-cannot-define-principle" ~category:"funind" + (fun (names,error) -> strbrk "Cannot define induction principle(s) for "++ + h 1 names ++ error) let warning_error names e = let e = process_vernac_interp_error e in @@ -282,33 +295,29 @@ let warning_error names e = match e with | ToShow e -> let e = process_vernac_interp_error e in - spc () ++ Errors.print e + spc () ++ CErrors.print e | _ -> if do_observe () then let e = process_vernac_interp_error e in - (spc () ++ Errors.print e) + (spc () ++ CErrors.print e) else mt () in match e with | Building_graph e -> - Feedback.msg_warning - (str "Cannot define graph(s) for " ++ - h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ - e_explain e) + let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in + warn_cannot_define_graph (names,e_explain e) | Defining_principle e -> - Feedback.msg_warning - (str "Cannot define principle(s) for "++ - h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ - e_explain e) + let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in + warn_cannot_define_principle (names,e_explain e) | _ -> raise e let error_error names e = let e = process_vernac_interp_error e in let e_explain e = match e with - | ToShow e -> spc () ++ Errors.print e - | _ -> if do_observe () then (spc () ++ Errors.print e) else mt () + | ToShow e -> spc () ++ CErrors.print e + | _ -> if do_observe () then (spc () ++ CErrors.print e) else mt () in match e with | Building_graph e -> @@ -376,7 +385,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error Array.iter (add_Function is_general) funs_kn; () end - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> on_error names e let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = @@ -466,7 +475,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation ); derive_inversion [fname] - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> (* No proof done *) () in @@ -861,6 +870,7 @@ let make_graph (f_ref:global_reference) = (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n),None)) nal + | Constrexpr.LocalPattern _ -> assert false ) nal_tas ) diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index e720691406..1c27bdface 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,5 +1,9 @@ open Misctypes +val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit + +val warn_cannot_define_principle : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit + val do_generate_principle : bool -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 2449678a13..f56e92414e 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -49,7 +49,7 @@ let locate_constant ref = let locate_with_msg msg f x = try f x - with Not_found -> raise (Errors.UserError("", msg)) + with Not_found -> raise (CErrors.UserError("", msg)) let filter_map filter f = @@ -73,7 +73,7 @@ let chop_rlambda_n = | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b | _ -> - raise (Errors.UserError("chop_rlambda_n", + raise (CErrors.UserError("chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) in chop_lambda_n [] @@ -85,7 +85,7 @@ let chop_rprod_n = else match rt with | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b - | _ -> raise (Errors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) + | _ -> raise (CErrors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] @@ -110,7 +110,7 @@ let const_of_id id = in try Constrintern.locate_reference princ_ref with Not_found -> - Errors.errorlabstrm "IndFun.const_of_id" + CErrors.errorlabstrm "IndFun.const_of_id" (str "cannot find " ++ Nameops.pr_id id) let def_of_const t = @@ -344,7 +344,7 @@ let pr_info f_info = (try Printer.pr_lconstr (Global.type_of_global_unsafe (ConstRef f_info.function_constant)) - with e when Errors.noncritical e -> mt ()) ++ fnl () ++ + with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ str "correctness_lemma := " ++ pr_ocst f_info.correctness_lemma ++ fnl () ++ @@ -371,7 +371,7 @@ let in_Function : function_info -> Libobject.obj = let find_or_none id = try Some - (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly (Pp.str "Not a constant") + (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant") ) with Not_found -> None @@ -399,7 +399,7 @@ let add_Function is_general f = and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind") and graph_ind = match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) - with | IndRef ind -> ind | _ -> Errors.anomaly (Pp.str "Not an inductive") + with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive") in let finfos = { function_constant = f; @@ -476,13 +476,13 @@ let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq" - with e when Errors.noncritical e -> raise (ToShow e) + with e when CErrors.noncritical e -> raise (ToShow e) let jmeq_refl () = try Coqlib.check_required_library Coqlib.jmeq_module_name; Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl" - with e when Errors.noncritical e -> raise (ToShow e) + with e when CErrors.noncritical e -> raise (ToShow e) let h_intros l = tclMAP (fun x -> Proofview.V82.of_tactic (Tactics.Simple.intro x)) l diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 1ff254f6ca..26fc88a604 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -8,7 +8,7 @@ open Tacexpr open Declarations -open Errors +open CErrors open Util open Names open Term @@ -65,16 +65,16 @@ let observe strm = let do_observe_tac s tac g = let goal = try Printer.pr_goal g - with e when Errors.noncritical e -> assert false + with e when CErrors.noncritical e -> assert false in try let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v with reraise -> - let reraise = Errors.push reraise in - let e = Cerrors.process_vernac_interp_error reraise in + let reraise = CErrors.push reraise in + let e = ExplainErr.process_vernac_interp_error reraise in observe (hov 0 (str "observation "++ s++str " raised exception " ++ - Errors.iprint e ++ str " on goal" ++ fnl() ++ goal )); + CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal )); iraise reraise;; @@ -90,7 +90,7 @@ let observe_tac s tac g = (* [nf_zeta] $\zeta$-normalization of a term *) let nf_zeta = - Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) Environ.empty_env Evd.empty @@ -585,7 +585,7 @@ let rec reflexivity_with_destruct_cases g = observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases ] | _ -> Proofview.V82.of_tactic reflexivity - with e when Errors.noncritical e -> Proofview.V82.of_tactic reflexivity + with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity in let eq_ind = make_eq () in let discr_inject = @@ -998,7 +998,7 @@ let invfun qhyp f = let f = match f with | ConstRef f -> f - | _ -> raise (Errors.UserError("",str "Not a function")) + | _ -> raise (CErrors.UserError("",str "Not a function")) in try let finfos = find_Function_infos f in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 99a165044c..de4210af5f 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -11,7 +11,7 @@ open Globnames open Tactics open Indfun_common -open Errors +open CErrors open Util open Constrexpr open Vernacexpr @@ -73,7 +73,7 @@ let ident_global_exist id = let ans = CRef (Libnames.Ident (Loc.ghost,id), None) in let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in true - with e when Errors.noncritical e -> false + with e when CErrors.noncritical e -> false (** [next_ident_fresh id] returns a fresh identifier (ie not linked in global env) with base [id]. *) @@ -785,10 +785,10 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) let params1 = try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1)) - with e when Errors.noncritical e -> [] in + with e when CErrors.noncritical e -> [] in let params2 = try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2)) - with e when Errors.noncritical e -> [] in + with e when CErrors.noncritical e -> [] in let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 95b4967faa..fa84e4ddf3 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -16,7 +16,7 @@ open Names open Libnames open Globnames open Nameops -open Errors +open CErrors open Util open Tacticals open Tacmach @@ -92,15 +92,15 @@ let const_of_ref = function let nf_zeta env = - Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) env Evd.empty let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) let clos_norm_flags flgs env sigma t = - Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in - clos_norm_flags Closure.betaiotazeta Environ.empty_env Evd.empty + CClosure.norm_val (CClosure.create_clos_infos flgs env) (CClosure.inject (Reductionops.nf_evar sigma t)) in + clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty @@ -161,7 +161,7 @@ let rec n_x_id ids n = let simpl_iter clause = reduce (Lazy - {rBeta=true;rIota=true;rZeta= true; rDelta=false; + {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=true;rDelta=false; rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]}) clause @@ -214,7 +214,7 @@ let print_debug_queue b e = begin let lmsg,goal = Stack.pop debug_queue in if b then - Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) + Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal)) else begin Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal)); @@ -238,9 +238,9 @@ let do_observe_tac s tac g = ignore(Stack.pop debug_queue); v with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in if not (Stack.is_empty debug_queue) - then print_debug_queue true (fst (Cerrors.process_vernac_interp_error reraise)); + then print_debug_queue true (fst (ExplainErr.process_vernac_interp_error reraise)); iraise reraise let observe_tac s tac g = @@ -441,7 +441,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = try check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id) end | Lambda(n,t,b) -> @@ -449,7 +449,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = try check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id) end | Case(ci,t,a,l) -> @@ -645,7 +645,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info = try check_not_nested (expr_info.f_id::expr_info.forbidden_ids) b; true - with e when Errors.noncritical e -> false + with e when CErrors.noncritical e -> false in if forbid then @@ -704,7 +704,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = try check_not_nested (expr_info.f_id::expr_info.forbidden_ids) a; false - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> true in let a' = infos.info in @@ -1281,12 +1281,12 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp | Some s -> s | None -> try add_suffix current_proof_name "_subproof" - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> anomaly (Pp.str "open_new_goal with an unamed theorem") in let na = next_global_ident_away name [] in if Termops.occur_existential gls_type then - Errors.error "\"abstract\" cannot handle existentials"; + CErrors.error "\"abstract\" cannot handle existentials"; let hook _ _ = let opacity = let na_ref = Libnames.Ident (Loc.ghost,na) in @@ -1516,13 +1516,13 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in + (* Refresh the global universes, now including those of _F *) + let evm = Evd.from_env (Global.env ()) in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in - let relation = - fst (*FIXME*)(interp_constr - env_with_pre_rec_args - (Evd.from_env env_with_pre_rec_args) - r) + let relation, evuctx = + interp_constr env_with_pre_rec_args evm r in + let evm = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref None in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) @@ -1534,11 +1534,13 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let stop = try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); false - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> begin if do_observe () - then Feedback.msg_debug (str "Cannot create equation Lemma " ++ Errors.print e) - else anomaly (Pp.str "Cannot create equation Lemma") + then Feedback.msg_debug (str "Cannot create equation Lemma " ++ CErrors.print e) + else CErrors.errorlabstrm "Cannot create equation Lemma" + (str "Cannot create equation lemma." ++ spc () ++ + str "This may be because the function is nested-recursive.") ; true end |