diff options
Diffstat (limited to 'plugins')
34 files changed, 183 insertions, 158 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index fd46d80695..aedecc15c1 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -23,7 +23,9 @@ open Pp open CErrors open Util open Proofview.Notations -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration let reference dir s = lazy (Coqlib.gen_reference "CC" dir s) @@ -155,7 +157,7 @@ let rec quantified_atom_of_constr env sigma nrels term = let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else - quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma (succ nrels) ff + quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff | _ -> let patts=patterns_of_constr env sigma nrels term in `Rule patts @@ -170,7 +172,7 @@ let litteral_of_constr env sigma term= else begin try - quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma 1 ff + quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff with Not_found -> `Other (decompose_term env sigma term) end @@ -192,10 +194,10 @@ let make_prb gls depth additionnal_terms = ignore (add_term state t)) additionnal_terms; List.iter (fun decl -> - let (id,_,e) = Context.Named.Declaration.to_tuple decl in + let id = NamedDecl.get_id decl in begin let cid=mkVar id in - match litteral_of_constr env sigma e with + match litteral_of_constr env sigma (NamedDecl.get_type decl) with `Eq (t,a,b) -> add_equality state cid a b | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b | `Other ph -> @@ -456,7 +458,7 @@ let cc_tactic depth additionnal_terms = end } let cc_fail gls = - errorlabstrm "Congruence" (Pp.str "congruence failed.") + user_err ~hdr:"Congruence" (Pp.str "congruence failed.") let congruence_tac depth l = Tacticals.New.tclORELSE diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 52a1351199..6f6811334d 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -10,7 +10,6 @@ open Cctac open Stdarg -open Constrarg DECLARE PLUGIN "cc_plugin" diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index a862423e99..f68c01b18b 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -90,8 +90,8 @@ let rec add_vars_of_simple_pattern globs = function (* Loc.raise loc (UserError ("simple_pattern",str "\"as\" is not allowed here"))*) | CPatOr (loc, _)-> - Loc.raise loc - (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here")) + Loc.raise ~loc + (UserError (Some "simple_pattern",str "\"(_ | _)\" is not allowed here")) | CPatDelimiters (_,_,p) -> add_vars_of_simple_pattern globs p | CPatCstr (_,_,pl1,pl2) -> @@ -328,7 +328,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = let _ = let expected = mib.Declarations.mind_nparams - num_params in if not (Int.equal (List.length params) expected) then - errorlabstrm "suppose it is" + user_err ~hdr:"suppose it is" (str "Wrong number of extra arguments: " ++ (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++ str "expected.") in @@ -348,7 +348,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp) | Thesis (For rec_occ) -> if not (Id.List.mem rec_occ pat_vars) then - errorlabstrm "suppose it is" + user_err ~hdr:"suppose it is" (str "Variable " ++ Nameops.pr_id rec_occ ++ str " does not occur in pattern."); Glob_term.GSort(Loc.ghost,GProp) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index d30fcf6033..e19dc86c45 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -32,6 +32,9 @@ open Misctypes open Sigma.Notations open Context.Named.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (* Strictness option *) let clear ids { it = goal; sigma } = @@ -43,7 +46,7 @@ let clear ids { it = goal; sigma } = let (hyps, concl) = try Evarutil.clear_hyps_in_evi env evdref sign cl ids with Evarutil.ClearDependencyError (id, _) -> - errorlabstrm "" (str "Cannot clear " ++ pr_id id) + user_err (str "Cannot clear " ++ pr_id id) in let sigma = !evdref in let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in @@ -247,7 +250,7 @@ let close_previous_case pts = let filter_hyps f gls = let filter_aux id = - let id = get_id id in + let id = NamedDecl.get_id id in if f id then tclIDTAC else @@ -357,8 +360,7 @@ let enstack_subsubgoals env se stack gls= let nlast=succ last in let (llast,holes,metas) = meta_aux nlast (mkMeta nlast :: lenv) q in - let open Context.Rel.Declaration in - (llast,holes,(nlast,special_nf gls (substl lenv (get_type decl)))::metas) in + (llast,holes,(nlast,special_nf gls (substl lenv (RelDecl.get_type decl)))::metas) in let (nlast,holes,nmetas) = meta_aux se.se_last_meta [] (List.rev rc) in let refiner = applist (appterm,List.rev holes) in @@ -821,9 +823,8 @@ let define_tac id args body gls = let cast_tac id_or_thesis typ gls = match id_or_thesis with - This id -> - let body = pf_get_hyp gls id |> get_value in - Proofview.V82.of_tactic (convert_hyp (of_tuple (id,body,typ))) gls + | This id -> + Proofview.V82.of_tactic (id |> pf_get_hyp gls |> NamedDecl.set_id id |> NamedDecl.set_type typ |> convert_hyp) gls | Thesis (For _ ) -> error "\"thesis for ...\" is not applicable here." | Thesis Plain -> @@ -1082,12 +1083,12 @@ let thesis_for obj typ per_info env= let cind,all_args=decompose_app typ in let ind,u = destInd cind in let _ = if not (eq_ind ind per_info.per_ind) then - errorlabstrm "thesis_for" + user_err ~hdr:"thesis_for" ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ str"cannot give an induction hypothesis (wrong inductive type).") in let params,args = List.chop per_info.per_nparams all_args in let _ = if not (List.for_all2 eq_constr params per_info.per_params) then - errorlabstrm "thesis_for" + user_err ~hdr:"thesis_for" ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ str "cannot give an induction hypothesis (wrong parameters).") in let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 6c17dcc4f1..18a35c6cfb 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -19,7 +19,7 @@ open Vernacexpr open Tok (* necessary for camlp4 *) open Pcoq.Constr -open Pcoq.Tactic +open Pltac open Ppdecl_proof let pr_goal gs = diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 index d4dc7e0eed..deadb3b4d5 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Constrarg +open Stdarg (*i camlp4deps: "grammar/grammar.cma" i*) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 19fda4aead..e1d6bb4a84 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -14,7 +14,6 @@ DECLARE PLUGIN "extraction_plugin" open Genarg open Stdarg -open Constrarg open Pcoq.Prim open Pp open Names diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index ff66d915f5..5e7d810c93 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -293,7 +293,7 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref) (*S Warning and Error messages. *) -let err s = errorlabstrm "Extraction" s +let err s = user_err ~hdr:"Extraction" s let warn_extraction_axiom_to_realize = CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction" diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 58744b5754..b34a364920 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -15,7 +15,8 @@ open Tacmach open Util open Declarations open Globnames -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration let qflag=ref true @@ -141,7 +142,7 @@ let build_atoms gl metagen side cciterm = end; let v = ind_hyps 0 i l gl in let g i _ decl = - build_rec env polarity (lift i (get_type decl)) in + build_rec env polarity (lift i (RelDecl.get_type decl)) in let f l = List.fold_left_i g (1-(List.length l)) () l in if polarity && (* we have a constant constructor *) @@ -152,7 +153,7 @@ let build_atoms gl metagen side cciterm = let var=mkMeta (metagen true) in let v =(ind_hyps 1 i l gl).(0) in let g i _ decl = - build_rec (var::env) polarity (lift i (get_type decl)) in + build_rec (var::env) polarity (lift i (RelDecl.get_type decl)) in List.fold_left_i g (2-(List.length l)) () v | Forall(_,b)-> let var=mkMeta (metagen true) in @@ -225,7 +226,7 @@ let build_formula side nam typ gl metagen= | And(_,_,_) -> Rand | Or(_,_,_) -> Ror | Exists (i,l) -> - let d = get_type (List.last (ind_hyps 0 i l gl).(0)) in + let d = RelDecl.get_type (List.last (ind_hyps 0 i l gl).(0)) in Rexists(m,d,trivial) | Forall (_,a) -> Rforall | Arrow (a,b) -> Rarrow in diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 95095b09cb..344a04a6aa 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -15,8 +15,8 @@ open Goptions open Tacticals open Tacinterp open Libnames -open Constrarg open Stdarg +open Tacarg open Pcoq.Prim DECLARE PLUGIN "ground_plugin" diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index ffb63af072..7ffc78928d 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -19,7 +19,8 @@ open Formula open Sequent open Globnames open Locus -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic @@ -36,12 +37,12 @@ let wrap n b continue seq gls= match nc with []->anomaly (Pp.str "Not the expected number of hyps") | nd::q-> - let id = get_id nd in + let id = NamedDecl.get_id nd in if occur_var env id (pf_concl gls) || List.exists (occur_var_in_decl env id) ctx then (aux (i-1) q (nd::ctx)) else - add_formula Hyp (VarRef id) (get_type nd) (aux (i-1) q (nd::ctx)) gls in + add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in let seq1=aux n nc [] in let seq2=if b then add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index b0ffc775b5..527f4f0b12 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -16,6 +16,8 @@ open Libnames open Globnames open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (* let msgnl = Pp.msgnl *) (* @@ -307,7 +309,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = try let witness = Int.Map.find i sub in if is_local_def decl then anomaly (Pp.str "can not redefine a rel!"); - (Termops.pop end_of_type,ctxt_size,mkLetIn (get_name decl, witness, get_type decl, witness_fun)) + (Termops.pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun)) with Not_found -> (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) ) @@ -938,8 +940,8 @@ let generalize_non_dep hyp g = ((* observe_tac "thin" *) (thin to_revert)) g -let id_of_decl decl = Nameops.out_name (get_name decl) -let var_of_decl decl = mkVar (id_of_decl decl) +let id_of_decl = RelDecl.get_name %> Nameops.out_name +let var_of_decl = id_of_decl %> mkVar let revert idl = tclTHEN (Proofview.V82.of_tactic (generalize (List.map mkVar idl))) @@ -1072,7 +1074,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (Name new_id) ) in - let fresh_decl = map_name fresh_id in + let fresh_decl = RelDecl.map_name fresh_id in let princ_info : elim_scheme = { princ_info with params = List.map fresh_decl princ_info.params; @@ -1119,11 +1121,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam ) in observe (str "full_params := " ++ - prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl))) + prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id) full_params ); observe (str "princ_params := " ++ - prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl))) + prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id) princ_params ); observe (str "fbody_with_full_params := " ++ @@ -1165,7 +1167,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let pte_to_fix,rev_info = List.fold_left_i (fun i (acc_map,acc_info) decl -> - let pte = get_name decl in + let pte = RelDecl.get_name decl in let infos = info_array.(i) in let type_args,_ = decompose_prod infos.types in let nargs = List.length type_args in @@ -1277,7 +1279,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (do_replace evd full_params (fix_info.idx + List.length princ_params) - (args_id@(List.map (fun decl -> Nameops.out_name (get_name decl)) princ_params)) + (args_id@(List.map (RelDecl.get_name %> Nameops.out_name) princ_params)) (all_funs.(fix_info.num_in_block)) fix_info.num_in_block all_funs @@ -1556,7 +1558,7 @@ let prove_principle_for_gen | _ -> assert false in (* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *) - let subst_constrs = List.map (fun decl -> mkVar (Nameops.out_name (get_name decl))) (pre_rec_arg@princ_info.params) in + let subst_constrs = List.map (get_name %> Nameops.out_name %> mkVar) (pre_rec_arg@princ_info.params) in let relation = substl subst_constrs relation in let input_type = substl subst_constrs rec_arg_type in let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in @@ -1584,7 +1586,7 @@ let prove_principle_for_gen ) g in - let args_ids = List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.args in + let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in let lemma = match !tcc_lemma_ref with | None -> error "No tcc proof !!" @@ -1631,7 +1633,7 @@ let prove_principle_for_gen [ observe_tac "start_tac" start_tac; h_intros - (List.rev_map (fun decl -> Nameops.out_name (get_name decl)) + (List.rev_map (get_name %> Nameops.out_name) (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) ); (* observe_tac "" *) Proofview.V82.of_tactic (assert_by @@ -1669,7 +1671,7 @@ let prove_principle_for_gen in let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in let predicates_names = - List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.predicates + List.map (get_name %> Nameops.out_name) princ_info.predicates in let pte_info = { proving_tac = @@ -1685,7 +1687,7 @@ let prove_principle_for_gen is_mes acc_inv fix_id (!tcc_list@(List.map - (fun decl -> (Nameops.out_name (get_name decl))) + (get_name %> Nameops.out_name) (princ_info.args@princ_info.params) )@ ([acc_rec_arg_id])) eqs ) @@ -1714,7 +1716,7 @@ let prove_principle_for_gen (* observe_tac "instanciate_hyps_with_args" *) (instanciate_hyps_with_args make_proof - (List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.branches) + (List.map (get_name %> Nameops.out_name) princ_info.branches) (List.rev args_ids) ) gl' diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 5e72b8672a..cc699e5d3d 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -14,6 +14,8 @@ open Functional_principles_proofs open Misctypes open Sigma.Notations +module RelDecl = Context.Rel.Declaration + exception Toberemoved_with_rel of int*constr exception Toberemoved @@ -38,7 +40,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Name x -> let id = Namegen.next_ident_away x avoid in Hashtbl.add tbl id x; - set_name (Name id) decl :: change_predicates_names (id::avoid) predicates + RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates | Anonymous -> anomaly (Pp.str "Anonymous property binder ")) in let avoid = (Termops.ids_of_context env_with_params ) in @@ -51,7 +53,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = (* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *) let change_predicate_sort i decl = let new_sort = sorts.(i) in - let args,_ = decompose_prod (get_type decl) in + let args,_ = decompose_prod (RelDecl.get_type decl) in let real_args = if princ_type_info.indarg_in_concl then List.tl args @@ -609,7 +611,7 @@ let build_scheme fas = try Smartlocate.global_with_alias f with Not_found -> - errorlabstrm "FunInd.build_scheme" + user_err ~hdr:"FunInd.build_scheme" (str "Cannot find " ++ Libnames.pr_reference f) in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in @@ -643,7 +645,7 @@ let build_case_scheme fa = let (_,f,_) = fa in try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) with Not_found -> - errorlabstrm "FunInd.build_case_scheme" + user_err ~hdr:"FunInd.build_case_scheme" (str "Cannot find " ++ Libnames.pr_reference f) in let first_fun,u = destConst funs in let funs_mp,funs_dp,_ = Names.repr_con first_fun in diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 42e4903155..6603a95a84 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -14,11 +14,11 @@ open Constrexpr open Indfun_common open Indfun open Genarg -open Constrarg +open Stdarg open Misctypes open Pcoq.Prim open Pcoq.Constr -open Pcoq.Tactic +open Pltac DECLARE PLUGIN "recdef_plugin" @@ -143,7 +143,7 @@ END module Gram = Pcoq.Gram module Vernac = Pcoq.Vernac_ -module Tactic = Pcoq.Tactic +module Tactic = Pltac type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 52179ae508..de2e5ea4e2 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -12,6 +12,9 @@ open Util open Glob_termops open Misctypes +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + let observe strm = if do_observe () then Feedback.msg_debug strm @@ -333,19 +336,20 @@ let raw_push_named (na,raw_value,raw_typ) env = match na with | Anonymous -> env | Name id -> - let value = Option.map (fun x-> fst (Pretyping.understand env (Evd.from_env env) x)) raw_value in - let typ,ctx = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in - let open Context.Named.Declaration in - Environ.push_named (of_tuple (id,value,typ)) env + let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in + (match raw_value with + | None -> + Environ.push_named (NamedDecl.LocalAssum (id,typ)) env + | Some value -> + Environ.push_named (NamedDecl.LocalDef (id, value, typ)) env) let add_pat_variables pat typ env : Environ.env = let rec add_pat_variables env pat typ : Environ.env = - let open Context.Rel.Declaration in observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); match pat with - | PatVar(_,na) -> Environ.push_rel (LocalAssum (na,typ)) env + | PatVar(_,na) -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env | PatCstr(_,c,patl,na) -> let Inductiveops.IndType(indf,indargs) = try Inductiveops.find_rectype env (Evd.from_env env) typ @@ -353,7 +357,7 @@ let add_pat_variables pat typ env : Environ.env = in let constructors = Inductiveops.get_constructors env indf in let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in - let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in + let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in List.fold_left2 add_pat_variables env patl (List.rev cs_args_types) in let new_env = add_pat_variables env pat typ in @@ -361,20 +365,28 @@ let add_pat_variables pat typ env : Environ.env = fst ( Context.Rel.fold_outside (fun decl (env,ctxt) -> - let _,v,t = Context.Rel.Declaration.to_tuple decl in - match Context.Rel.Declaration.get_name decl with - | Anonymous -> assert false - | Name id -> + let open Context.Rel.Declaration in + match decl with + | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false + | LocalAssum (Name id, t) -> + let new_t = substl ctxt t in + observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ + str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ + str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () + ); + let open Context.Named.Declaration in + (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt) + | LocalDef (Name id, v, t) -> let new_t = substl ctxt t in - let new_v = Option.map (substl ctxt) v in + let new_v = substl ctxt v in observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++ - Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++ - Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ()) + str "old value := " ++ Printer.pr_lconstr v ++ fnl () ++ + str "new value := " ++ Printer.pr_lconstr new_v ++ fnl () ); let open Context.Named.Declaration in - (Environ.push_named (of_tuple (id,new_v,new_t)) env,mkVar id::ctxt) + (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) ) (Environ.rel_context new_env) ~init:(env,[]) @@ -402,8 +414,7 @@ let rec pattern_to_term_and_type env typ = function in let constructors = Inductiveops.get_constructors env indf in let constructor = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in - let open Context.Rel.Declaration in - let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in + let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in let _,cstl = Inductiveops.dest_ind_family indf in let csta = Array.of_list cstl in let implicit_args = @@ -602,10 +613,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in let new_env = - let open Context.Named.Declaration in match n with Anonymous -> env - | Name id -> Environ.push_named (of_tuple (id,Some v_as_constr,v_type)) env + | Name id -> Environ.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_letin n) v_res b_res @@ -621,7 +631,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> - errorlabstrm "" (str "Cannot find the inductive associated to " ++ + user_err (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ Printer.pr_glob_constr rt ++ str ". try again with a cast") in @@ -653,7 +663,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> - errorlabstrm "" (str "Cannot find the inductive associated to " ++ + user_err (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ Printer.pr_glob_constr rt ++ str ". try again with a cast") in @@ -976,8 +986,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (fun acc var_as_constr arg -> if isRel var_as_constr then - let open Context.Rel.Declaration in - let na = get_name (Environ.lookup_rel (destRel var_as_constr) env) in + let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in match na with | Anonymous -> acc | Name id' -> @@ -1189,7 +1198,7 @@ let rec compute_cst_params relnames params = function | GSort _ -> params | GHole _ -> params | GIf _ | GRec _ | GCast _ -> - raise (UserError("compute_cst_params", str "Not handled case")) + raise (UserError(Some "compute_cst_params", str "Not handled case")) and compute_cst_params_from_app acc (params,rtl) = match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 01e5ef7fba..4e561fc7e5 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -406,7 +406,7 @@ let is_free_in id = | GIf(_,cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 - | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ -> false | GHole _ -> false | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t @@ -502,7 +502,7 @@ let replace_var_by_term x_id term = replace_var_by_pattern lhs, replace_var_by_pattern rhs ) - | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ -> rt | GHole _ -> rt | GCast(loc,b,c) -> @@ -655,7 +655,7 @@ let zeta_normalize = zeta_normalize_term lhs, zeta_normalize_term rhs ) - | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ -> rt | GHole _ -> rt | GCast(loc,b,c) -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 18817f504c..99b04898ba 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,4 +1,3 @@ -open Context.Rel.Declaration open CErrors open Util open Names @@ -13,11 +12,13 @@ open Misctypes open Decl_kinds open Sigma.Notations +module RelDecl = Context.Rel.Declaration + let is_rec_info scheme_info = let test_branche min acc decl = acc || ( let new_branche = - it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (get_type decl))) in + it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (RelDecl.get_type decl))) in let free_rels_in_br = Termops.free_rels new_branche in let max = min + scheme_info.Tactics.npredicates in Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br @@ -42,7 +43,7 @@ let functional_induction with_clean c princl pat = let finfo = (* we first try to find out a graph on f *) try find_Function_infos c' with Not_found -> - errorlabstrm "" (str "Cannot find induction information on "++ + user_err (str "Cannot find induction information on "++ Printer.pr_lconstr (mkConst c') ) in match Tacticals.elimination_sort_of_goal g with @@ -70,11 +71,11 @@ let functional_induction with_clean c princl pat = (b,a) (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *) with Not_found -> (* This one is neither defined ! *) - errorlabstrm "" (str "Cannot find induction principle for " + user_err (str "Cannot find induction principle for " ++Printer.pr_lconstr (mkConst c') ) in (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g') - | _ -> raise (UserError("",str "functional induction must be used with a function" )) + | _ -> raise (UserError(None,str "functional induction must be used with a function" )) end | Some ((princ,binding)) -> princ,binding,Tacmach.pf_unsafe_type_of g princ,g @@ -175,7 +176,7 @@ let build_newrecursive l = match body_opt with | Some body -> (fixna,bll,ar,body) - | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") ) l in build_newrecursive l' @@ -321,7 +322,7 @@ let error_error names e = in match e with | Building_graph e -> - errorlabstrm "" + user_err (str "Cannot define graph(s) for " ++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ e_explain e) @@ -391,7 +392,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> - let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in Command.do_definition fname (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl @@ -630,7 +631,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof | _ -> assert false in let fixpoint_exprl = [fixpoint_expr] in - let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let using_lemmas = [] in let pre_hook pconstants = @@ -656,7 +657,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof let fixpoint_exprl = [fixpoint_expr] in let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let using_lemmas = [] in - let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in let pre_hook pconstants = generate_principle (ref (Evd.from_env (Global.env ()))) @@ -834,9 +835,9 @@ let make_graph (f_ref:global_reference) = | ConstRef c -> begin try c,Global.lookup_constant c with Not_found -> - raise (UserError ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) ) + raise (UserError (None,str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) ) end - | _ -> raise (UserError ("", str "Not a function reference") ) + | _ -> raise (UserError (None, str "Not a function reference") ) in (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom !" diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index f56e92414e..a45effb167 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 (CErrors.UserError("", msg)) + with Not_found -> raise (CErrors.UserError(None, 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 (CErrors.UserError("chop_rlambda_n", + raise (CErrors.UserError(Some "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 (CErrors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) + | _ -> raise (CErrors.UserError(Some "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 -> - CErrors.errorlabstrm "IndFun.const_of_id" + CErrors.user_err ~hdr:"IndFun.const_of_id" (str "cannot find " ++ Nameops.pr_id id) let def_of_const t = diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 26fc88a604..c8b4e48337 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -23,6 +23,8 @@ open Misctypes open Termops open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (* Some pretty printing function for debugging purpose *) let pr_binding prc = @@ -137,7 +139,7 @@ let generate_type evd g_to_f f graph i = let fun_ctxt,res_type = match ctxt with | [] | [_] -> anomaly (Pp.str "Not a valid context") - | decl :: fun_ctxt -> fun_ctxt, get_type decl + | decl :: fun_ctxt -> fun_ctxt, RelDecl.get_type decl in let rec args_from_decl i accu = function | [] -> accu @@ -148,7 +150,7 @@ let generate_type evd g_to_f f graph i = args_from_decl (succ i) (t :: accu) l in (*i We need to name the vars [res] and [fv] i*) - let filter = fun decl -> match get_name decl with + let filter = fun decl -> match RelDecl.get_name decl with | Name id -> Some id | Anonymous -> None in @@ -269,7 +271,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (fun decl -> List.map (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id)) - (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (get_type decl))))) + (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (RelDecl.get_type decl))))) ) branches in @@ -399,7 +401,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes | hres::res::decl::ctxt -> let res = Termops.it_mkLambda_or_LetIn (Termops.it_mkProd_or_LetIn concl [hres;res]) - (LocalAssum (get_name decl, get_type decl) :: ctxt) + (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt) in res ) @@ -415,7 +417,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let params_bindings,avoid = List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in p::bindings,id::avoid ) ([],pf_ids_of_hyps g) @@ -425,7 +427,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let lemmas_bindings = List.rev (fst (List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in (nf_zeta p)::bindings,id::avoid) ([],avoid) princ_infos.predicates @@ -682,7 +684,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (fun decl -> List.map (fun id -> id) - (generate_fresh_id (Id.of_string "y") ids (nb_prod (get_type decl))) + (generate_fresh_id (Id.of_string "y") ids (nb_prod (RelDecl.get_type decl))) ) branches in @@ -998,7 +1000,7 @@ let invfun qhyp f = let f = match f with | ConstRef f -> f - | _ -> raise (CErrors.UserError("",str "Not a function")) + | _ -> raise (CErrors.UserError(None,str "Not a function")) in try let finfos = find_Function_infos f in @@ -1043,19 +1045,19 @@ let invfun qhyp f g = functional_inversion kn hid f2 f_correct g with | Failure "" -> - errorlabstrm "" (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function") + user_err (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function") | Option.IsNone -> if do_observe () then error "Cannot use equivalence with graph for any side of the equality" - else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) + else user_err (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) | Not_found -> if do_observe () then error "No graph found for any side of equality" - else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) + else user_err (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) end - | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ") + | _ -> user_err (Ppconstr.pr_id hid ++ str " must be an equality ") end) qhyp end diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index de4210af5f..7cbe787c3b 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -26,6 +26,8 @@ open Glob_termops open Decl_kinds open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (** {1 Utilities} *) (** {2 Useful operations on constr and glob_constr} *) @@ -57,8 +59,8 @@ let understand = Pretyping.understand (Global.env()) Evd.empty let id_of_name = function Anonymous -> Id.of_string "H" | Name id -> id;; -let name_of_string str = Name (Id.of_string str) -let string_of_name nme = Id.to_string (id_of_name nme) +let name_of_string = Id.of_string %> Name.mk_name +let string_of_name = id_of_name %> Id.to_string (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *) let isVarf f x = @@ -137,7 +139,7 @@ let showind (id:Id.t) = let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in List.iter (fun decl -> print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":"); - prconstr (get_type decl); print_string "\n") + prconstr (RelDecl.get_type decl); print_string "\n") ib1.mind_arity_ctxt; Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1); Array.iteri @@ -460,12 +462,12 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in let _ = prstr "\notherprms1:\n" in let _ = - List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : "); - prconstr (get_type decl); prstr "\n") + List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : "); + prconstr (RelDecl.get_type decl); prstr "\n") otherprms1 in let _ = prstr "\notherprms2:\n" in let _ = - List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : "); prconstr (get_type decl); prstr "\n") + List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : "); prconstr (RelDecl.get_type decl); prstr "\n") otherprms2 in { ident=id; @@ -827,7 +829,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = List.fold_left (fun (acc,env) decl -> let nm = Context.Rel.Declaration.get_name decl in - let c = get_type decl in + let c = RelDecl.get_type decl in let typ = Constrextern.extern_constr false env Evd.empty c in let newenv = Environ.push_rel (LocalAssum (nm,c)) env in CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) @@ -901,7 +903,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info = locate_constant f_ref in try find_Function_infos (kn_of_id id) with Not_found -> - errorlabstrm "indfun" (Nameops.pr_id id ++ str " has no functional scheme") + user_err ~hdr:"indfun" (Nameops.pr_id id ++ str " has no functional scheme") (** [merge id1 id2 args1 args2 id] builds and declares a new inductive type called [id], representing the merged graphs of both graphs diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 62f3071151..f43251bc50 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -307,7 +307,7 @@ let check_not_nested forbidden e = | Rel _ -> () | Var x -> if Id.List.mem x forbidden - then errorlabstrm "Recdef.check_not_nested" + then user_err ~hdr:"Recdef.check_not_nested" (str "check_not_nested: failure " ++ pr_id x) | Meta _ | Evar _ | Sort _ -> () | Cast(e,_,t) -> check_not_nested e;check_not_nested t @@ -327,7 +327,7 @@ let check_not_nested forbidden e = try check_not_nested e with UserError(_,p) -> - errorlabstrm "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p) + user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p) (* ['a info] contains the local information for traveling *) type 'a infos = @@ -377,7 +377,7 @@ type journey_info = let rec add_vars forbidden e = match kind_of_term e with | Var x -> x::forbidden - | _ -> fold_constr add_vars forbidden e + | _ -> Term.fold_constr add_vars forbidden e let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = @@ -442,7 +442,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = 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 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) + user_err ~hdr:"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) -> begin @@ -450,7 +450,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = 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 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) + user_err ~hdr:"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) -> begin @@ -478,7 +478,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = jinfo.apP (f,args) expr_info continuation_tac in travel_args jinfo expr_info.is_main_branch new_continuation_tac new_infos - | Case _ -> errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") + | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_lconstr expr_info.info) end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} @@ -723,8 +723,8 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = (List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l) )) with - | UserError("Refiner.thensn_tac3",_) - | UserError("Refiner.tclFAIL_s",_) -> + | UserError(Some "Refiner.thensn_tac3",_) + | UserError(Some "Refiner.tclFAIL_s",_) -> (observe_tac (str "is computable " ++ Printer.pr_lconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} ) )) g diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 027f690fca..79020ed037 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -16,7 +16,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Constrarg +open Stdarg +open Tacarg DECLARE PLUGIN "micromega_plugin" diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d625e3076a..1afc6500b7 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -30,6 +30,7 @@ open Misctypes open Proofview.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration module OmegaSolver = Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -1697,8 +1698,8 @@ let destructure_hyps = let rec loop = function | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega) | decl::lit -> - let (i,_,t) = to_tuple decl in - begin try match destructurate_prop t with + let i = NamedDecl.get_id decl in + begin try match destructurate_prop (NamedDecl.get_type decl) with | Kapp(False,[]) -> elim_id i | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit | Kapp(Or,[t1;t2]) -> @@ -1808,13 +1809,13 @@ let destructure_hyps = match destructurate_type (pf_nf typ) with | Kapp(Nat,_) -> (Tacticals.New.tclTHEN - (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) - decl)) + (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) + decl)) (loop lit)) | Kapp(Z,_) -> (Tacticals.New.tclTHEN - (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) - decl)) + (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) + decl)) (loop lit)) | _ -> loop lit end diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 5647fbf9fc..27115abecc 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -19,7 +19,7 @@ DECLARE PLUGIN "omega_plugin" open Names open Coq_omega -open Constrarg +open Stdarg let eval_tactic name = let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index fd87d5b7d3..e7e6ecef98 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -13,7 +13,8 @@ open Misctypes open Tacexpr open Geninterp open Quote -open Constrarg +open Stdarg +open Tacarg DECLARE PLUGIN "quote_plugin" diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 830dc54ddb..2f38688d1f 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -12,7 +12,7 @@ DECLARE PLUGIN "romega_plugin" open Names open Refl_omega -open Constrarg +open Stdarg let eval_tactic name = let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 4ed9079517..367a133330 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -263,7 +263,7 @@ let rtauto_tac gls= let _= if Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) gl != InProp - then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in + then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in let glf=make_form gamma gls gl in let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in let formula= @@ -282,7 +282,7 @@ let rtauto_tac gls= let prf = try project (search_fun (init_state [] formula)) with Not_found -> - errorlabstrm "rtauto" (Pp.str "rtauto couldn't find any proof") in + user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in let search_end_time = System.get_time () in let _ = if !verbose then begin diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 216eb8b373..0987c44ae2 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -15,9 +15,9 @@ open Printer open Newring_ast open Newring open Stdarg -open Constrarg +open Tacarg open Pcoq.Constr -open Pcoq.Tactic +open Pltac DECLARE PLUGIN "newring_plugin" diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 90f5f8e63d..657efe175b 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -79,7 +79,7 @@ let add_map s m = protect_maps := String.Map.add s m !protect_maps let lookup_map map = try String.Map.find map !protect_maps with Not_found -> - errorlabstrm"lookup_map"(str"map "++qs map++str"not found") + user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found") let protect_red map env sigma c = kl (create_clos_infos all env) @@ -124,8 +124,8 @@ let closed_term_ast l = let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in TacFun([Some(Id.of_string"t")], TacML(Loc.ghost,tacname, - [TacGeneric (Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None)); - TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l)])) + [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None)); + TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)])) (* let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" *) @@ -348,13 +348,13 @@ let find_ring_structure env sigma l = let check c = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then - errorlabstrm "ring" + user_err ~hdr:"ring" (str"arguments of ring_simplify do not have all the same type") in List.iter check cl'; (try ring_for_carrier ty with Not_found -> - errorlabstrm "ring" + user_err ~hdr:"ring" (str"cannot find a declared ring structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false @@ -828,13 +828,13 @@ let find_field_structure env sigma l = let check c = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then - errorlabstrm "field" + user_err ~hdr:"field" (str"arguments of field_simplify do not have all the same type") in List.iter check cl'; (try field_for_carrier ty with Not_found -> - errorlabstrm "field" + user_err ~hdr:"field" (str"cannot find a declared field structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index a34fa4cae7..c265103a65 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -19,7 +19,8 @@ open Names open Pp open Pcoq open Genarg -open Constrarg +open Stdarg +open Tacarg open Term open Vars open Topconstr @@ -41,7 +42,7 @@ open Proofview.Notations open Tacinterp open Pretyping open Constr -open Tactic +open Pltac open Extraargs open Ppconstr open Printer @@ -61,8 +62,8 @@ DECLARE PLUGIN "ssrmatching_plugin" type loc = Loc.t let dummy_loc = Loc.ghost -let errorstrm = CErrors.errorlabstrm "ssrmatching" -let loc_error loc msg = CErrors.user_err_loc (loc, msg, str msg) +let errorstrm = CErrors.user_err ~hdr:"ssrmatching" +let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg) let ppnl = Feedback.msg_info (* 0 cost pp function. Active only if env variable SSRDEBUG is set *) diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index e18d19ced4..ed8cc6ab02 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -52,8 +52,8 @@ let interp_ascii_string dloc s = if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2] then int_of_string s else - user_err_loc (dloc,"interp_ascii_string", - str "Expects a single character or a three-digits ascii code.") in + user_err ~loc:dloc ~hdr:"interp_ascii_string" + (str "Expects a single character or a three-digits ascii code.") in interp_ascii dloc p let uninterp_ascii r = diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index a9eb126b4f..ab262fea70 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -47,8 +47,8 @@ let nat_of_int dloc n = mk_nat ref_O n end else - user_err_loc (dloc, "nat_of_int", - str "Cannot interpret a negative number as a number of type nat") + user_err ~hdr:"nat_of_int" + (str "Cannot interpret a negative number as a number of type nat") (************************************************************************) (* Printing via scopes *) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index f65f9b7910..a25ddb0622 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -100,7 +100,7 @@ let int31_of_pos_bigint dloc n = GApp (dloc, ref_construct, List.rev (args 31 n)) let error_negative dloc = - CErrors.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.") + CErrors.user_err ~loc:dloc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.") let interp_int31 dloc n = if is_pos_or_zero n then @@ -189,7 +189,7 @@ let bigN_of_pos_bigint dloc n = GApp (dloc, ref_constructor, args) let bigN_error_negative dloc = - CErrors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.") + CErrors.user_err ~loc:dloc ~hdr:"interp_bigN" (Pp.str "bigN are only non-negative numbers.") let interp_bigN dloc n = if is_pos_or_zero n then diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 60803a369a..b7b5fb8a58 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -57,8 +57,8 @@ let pos_of_bignat dloc x = pos_of x let error_non_positive dloc = - user_err_loc (dloc, "interp_positive", - str "Only strictly positive numbers in type \"positive\".") + user_err ~loc:dloc ~hdr:"interp_positive" + (str "Only strictly positive numbers in type \"positive\".") let interp_positive dloc n = if is_strictly_pos n then pos_of_bignat dloc n @@ -113,7 +113,7 @@ let n_of_binnat dloc pos_or_neg n = GRef (dloc, glob_N0, None) let error_negative dloc = - user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".") + user_err ~loc:dloc ~hdr:"interp_N" (str "No negative numbers in type \"N\".") let n_of_int dloc n = if is_pos_or_zero n then n_of_binnat dloc true n |