diff options
Diffstat (limited to 'plugins')
28 files changed, 184 insertions, 208 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 9c1882dc9a..aad3967f6d 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -12,8 +12,8 @@ open Constr open Context open Context.Named.Declaration -let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Entries.const_entry_body) - : Safe_typing.private_constants Entries.const_entry_body = +let map_const_entry_body (f:constr->constr) (x: Evd.side_effects Entries.const_entry_body) + : Evd.side_effects Entries.const_entry_body = Future.chain x begin fun ((b,ctx),fx) -> (f b , ctx) , fx end @@ -22,11 +22,11 @@ let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Ent (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] and [lemma] as the proof. *) -let start_deriving f suchthat lemma = +let start_deriving f suchthat name : Lemmas.t = let env = Global.env () in let sigma = Evd.from_env env in - let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in + let kind = Decl_kinds.(Global ImportDefaultBehavior,false,DefinitionBody Definition) in (* create a sort variable for the type of [f] *) (* spiwack: I don't know what the rigidity flag does, picked the one @@ -48,7 +48,6 @@ let start_deriving f suchthat lemma = (* The terminator handles the registering of constants when the proof is closed. *) let terminator com = - let open Proof_global in (* Extracts the relevant information from the proof. [Admitted] and [Save] result in user errors. [opaque] is [true] if the proof was concluded by [Qed], and [false] if [Defined]. [f_def] @@ -56,10 +55,10 @@ let start_deriving f suchthat lemma = [suchthat], respectively. *) let (opaque,f_def,lemma_def) = match com with - | Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") - | Proved (_,Some _,_) -> + | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") + | Lemmas.Proved (_,Some _,_) -> CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.") - | Proved (opaque, None, obj) -> + | Lemmas.Proved (opaque, None, obj) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> opaque <> Proof_global.Transparent , f_def , lemma_def @@ -97,12 +96,11 @@ let start_deriving f suchthat lemma = Entries.DefinitionEntry lemma_def , Decl_kinds.(IsProof Proposition) in - ignore (Declare.declare_constant lemma lemma_def) - in + ignore (Declare.declare_constant name lemma_def) + in - let terminator = Proof_global.make_terminator terminator in - let pstate = Proof_global.start_dependent_proof lemma kind goals terminator in - Proof_global.modify_proof begin fun p -> - let p,_,() = Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in - p - end pstate + let terminator ?hook _ = Lemmas.Internal.make_terminator terminator in + let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in + Lemmas.pf_map (Proof_global.map_proof begin fun p -> + Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p + end) lemma diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index 6bb923118e..ffbc726e22 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -12,4 +12,8 @@ (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] and [lemma] as the proof. *) -val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.t +val start_deriving + : Names.Id.t + -> Constrexpr.constr_expr + -> Names.Id.t + -> Lemmas.t diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index 526989fdf3..de3fb9f11f 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -18,11 +18,11 @@ DECLARE PLUGIN "derive_plugin" { -let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]),VtLater) +let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[])) } VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof | [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - { Derive.(start_deriving f suchthat lemma) } + { Derive.start_deriving f suchthat lemma } END diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index c5439ffaf6..4cd34100bc 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -752,13 +752,13 @@ let extract_and_compile l = (* Show the extraction of the current ongoing proof *) let show_extraction ~pstate = init ~inner:true false false; - let prf = Proof_global.give_me_the_proof pstate in + let prf = Proof_global.get_proof pstate in let sigma, env = Pfedit.get_current_context pstate in let trms = Proof.partial_proof prf in let extr_term t = let ast, ty = extract_constr env sigma t in let mp = Lib.current_mp () in - let l = Label.of_id (Proof_global.get_current_proof_name pstate) in + let l = Label.of_id (Proof_global.get_proof_name pstate) in let fake_ref = ConstRef (Constant.make2 mp l) in let decl = Dterm (fake_ref, ast, ty) in print_one_decl [] mp decl diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index e38ea992ab..b8e1286b9e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -990,21 +990,19 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num ] in (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) - let pstate = Lemmas.start_proof + let lemma = Lemmas.start_lemma (*i The next call to mk_equation_id is valid since we are constructing the lemma Ensures by: obvious i*) (mk_equation_id f_id) - (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) + Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem) evd lemma_type in - let pstate,_ = Pfedit.by (Proofview.V82.tactic prove_replacement) pstate in - let ontop = Proof_global.push ~ontop:None pstate in - ignore(Lemmas.save_proof_proved ?proof:None ~ontop ~opaque:Proof_global.Transparent ~idopt:None); + let lemma,_ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in + let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in evd - let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g = let equation_lemma = try @@ -1725,11 +1723,3 @@ let prove_principle_for_gen ] gl - - - - - - - - diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 7b26cb0c74..5363dc9a02 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -308,16 +308,16 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in evd := sigma; let hook = Lemmas.mk_hook (hook new_principle_type) in - let pstate = - Lemmas.start_proof + let lemma = + Lemmas.start_lemma new_princ_name - (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) + Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) !evd (EConstr.of_constr new_principle_type) in (* let _tim1 = System.get_time () in *) let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in - let pstate,_ = Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)) pstate in + let lemma,_ = Lemmas.by (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)) lemma in (* let _tim2 = System.get_time () in *) (* begin *) (* let dur1 = System.time_difference tim1 tim2 in *) @@ -325,7 +325,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* end; *) let open Proof_global in - let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pstate in + let { id; entries; persistence } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in match entries with | [entry] -> (id,(entry,persistence)), hook @@ -471,7 +471,7 @@ let get_funs_constant mp = exception No_graph_found exception Found_type of int -let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_constants definition_entry list = +let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects definition_entry list = let env = Global.env () in let funs = List.map fst fas in let first_fun = List.hd funs in @@ -597,7 +597,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ in {const with const_entry_body = - (Future.from_val (Safe_typing.mk_pure_proof princ_body)); + (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects)); const_entry_type = Some scheme_type } ) diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 97f9acdb3a..759c522820 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -34,7 +34,7 @@ val generate_functional_principle : exception No_graph_found val make_scheme : Evd.evar_map ref -> - (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list + (pconstant*Sorts.family) list -> Evd.side_effects Entries.definition_entry list val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 833ff9f1ed..c217ed8b1d 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -186,14 +186,14 @@ let classify_as_Fixpoint recsl = let classify_funind recsl = match classify_as_Fixpoint recsl with - | Vernacextend.VtSideff ids, _ + | Vernacextend.VtSideff (ids, _) when is_proof_termination_interactively_checked recsl -> - Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) + Vernacextend.(VtStartProof (GuaranteesOpacity, ids)) | x -> x let is_interactive recsl = match classify_funind recsl with - | Vernacextend.VtStartProof _, _ -> true + | Vernacextend.VtStartProof _ -> true | _ -> false } @@ -243,7 +243,7 @@ let warning_error names e = VERNAC COMMAND EXTEND NewFunctionalScheme | ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] - => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) } + => { Vernacextend.(VtSideff(List.map pi1 fas, VtLater)) } -> { begin try @@ -275,7 +275,7 @@ END VERNAC COMMAND EXTEND NewFunctionalCase | ["Functional" "Case" fun_scheme_arg(fas) ] - => { Vernacextend.(VtSideff[pi1 fas], VtLater) } + => { Vernacextend.(VtSideff([pi1 fas], VtLater)) } -> { Functional_principles_types.build_case_scheme fas } END diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 4c67d65816..201d953692 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1299,10 +1299,10 @@ let rec rebuild_return_type rt = | Constrexpr.CProdN(n,t') -> CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t') | Constrexpr.CLetIn(na,v,t,t') -> - CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') + CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous], Constrexpr.Default Decl_kinds.Explicit, rt)], - CAst.make @@ Constrexpr.CSort(GType [])) + CAst.make @@ Constrexpr.CSort(UAnonymous {rigid=true})) let do_build_inductive evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 241da053b7..d710f4490d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -417,7 +417,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ComDefinition.do_definition ~program_mode:false fname - (Decl_kinds.Global,false,Decl_kinds.Definition) pl + Decl_kinds.(Global ImportDefaultBehavior,false,Definition) pl bl None body (Some ret_type); let evd,rev_pconstants = List.fold_left @@ -434,7 +434,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in None, evd,List.rev rev_pconstants | _ -> - ComFixpoint.do_fixpoint Global false fixpoint_exprl; + ComFixpoint.do_fixpoint (Global ImportDefaultBehavior) false fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> @@ -634,9 +634,9 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex let do_generate_principle_aux pconstants on_error register_built interactive_proof - (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option = + (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Lemmas.t option = List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; - let pstate, _is_struct = + let lemma, _is_struct = match fixpoint_exprl with | [((_,Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)},_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr = @@ -702,7 +702,7 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro (* ok all the expressions are structural *) let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let is_rec = List.exists (is_rec fix_names) recdefs in - let pstate,evd,pconstants = + let lemma,evd,pconstants = if register_built then register_struct is_rec fixpoint_exprl else None, Evd.from_env (Global.env ()), pconstants @@ -720,9 +720,9 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro (Functional_principles_proofs.prove_princ_for_struct evd interactive_proof); if register_built then begin derive_inversion fix_names; end; - pstate, true + lemma, true in - pstate + lemma let rec add_args id new_args = CAst.map (function | CRef (qid,_) as b -> @@ -911,18 +911,18 @@ let make_graph (f_ref : GlobRef.t) = (* *************** statically typed entrypoints ************************* *) -let do_generate_principle_interactive fixl : Proof_global.t = +let do_generate_principle_interactive fixl : Lemmas.t = match do_generate_principle_aux [] warning_error true true fixl with - | Some pstate -> pstate + | Some lemma -> lemma | None -> - CErrors.anomaly - (Pp.str"indfun: leaving no open proof in interactive mode") + CErrors.anomaly + (Pp.str"indfun: leaving no open proof in interactive mode") let do_generate_principle fixl : unit = match do_generate_principle_aux [] warning_error true false fixl with - | Some _pstate -> - CErrors.anomaly - (Pp.str"indfun: leaving a goal open in non-interactive mode") + | Some _lemma -> + CErrors.anomaly + (Pp.str"indfun: leaving a goal open in non-interactive mode") | None -> () diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 1ba245a45d..3bc52272ac 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -10,7 +10,7 @@ val do_generate_principle : val do_generate_principle_interactive : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - Proof_global.t + Lemmas.t val functional_induction : bool -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 48cf040919..6d9690096f 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -124,26 +124,20 @@ open Declare let definition_message = Declare.definition_message -let get_locality = function -| Discharge -> true -| Local -> true -| Global -> false - let save id const ?hook uctx (locality,_,kind) = let fix_exn = Future.fix_exn_of const.const_entry_body in - let l,r = match locality with - | Discharge when Lib.sections_are_opened () -> + let r = match locality with + | Discharge -> let k = Kindops.logical_kind_of_goal_kind kind in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in - (Local, VarRef id) - | Discharge | Local | Global -> - let local = get_locality locality in + VarRef id + | Global local -> let k = Kindops.logical_kind_of_goal_kind kind in let kn = declare_constant id ~local (DefinitionEntry const, k) in - (locality, ConstRef kn) + ConstRef kn in - Lemmas.call_hook ?hook ~fix_exn uctx [] l r; + Lemmas.call_hook ?hook ~fix_exn uctx [] locality r; definition_message id let with_full_print f a = diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 9670cf1fa7..4078c34331 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -44,7 +44,7 @@ val jmeq_refl : unit -> EConstr.constr val save : Id.t - -> Safe_typing.private_constants Entries.definition_entry + -> Evd.side_effects Entries.definition_entry -> ?hook:Lemmas.declaration_hook -> UState.t -> Decl_kinds.goal_kind diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 03568fc6c7..857b7df96f 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -803,15 +803,15 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list i*) let lem_id = mk_correct_id f_id in let (typ,_) = lemmas_types_infos.(i) in - let pstate = Lemmas.start_proof + let lemma = Lemmas.start_lemma lem_id - (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem))) + Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) !evd typ in - let pstate = fst @@ Pfedit.by + let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") - (proving_tac i))) pstate in - let () = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None in + (proving_tac i))) lemma in + let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in let finfo = find_Function_infos (fst f_as_constant) in (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *) let _,lem_cst_constr = Evd.fresh_global @@ -865,13 +865,13 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list Ensures by: obvious i*) let lem_id = mk_complete_id f_id in - let pstate = Lemmas.start_proof lem_id - (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma + let lemma = Lemmas.start_lemma lem_id + Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma (fst lemmas_types_infos.(i)) in - let pstate = fst (Pfedit.by + let lemma = fst (Lemmas.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") - (proving_tac i))) pstate) in - let () = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None in + (proving_tac i))) lemma) in + let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in let finfo = find_Function_infos (fst f_as_constant) in let _,lem_cst_constr = Evd.fresh_global (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index e2321d233c..17d962f30f 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -34,7 +34,6 @@ open Declare open Decl_kinds open Tacred open Goal -open Pfedit open Glob_term open Pretyping open Termops @@ -72,7 +71,8 @@ let declare_fun f_id kind ?univs value = let ce = definition_entry ?univs value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; -let defined pstate = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None +let defined lemma = + Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None let def_of_const t = match (Constr.kind t) with @@ -1221,7 +1221,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a end let get_current_subgoals_types pstate = - let p = Proof_global.give_me_the_proof pstate in + let p = Proof_global.get_proof pstate in let Proof.{ goals=sgs; sigma; _ } = Proof.data p in sigma, List.map (Goal.V82.abstract_type sigma) sgs @@ -1281,8 +1281,8 @@ let clear_goals sigma = List.map clear_goal -let build_new_goal_type pstate = - let sigma, sub_gls_types = get_current_subgoals_types pstate in +let build_new_goal_type lemma = + let sigma, sub_gls_types = Lemmas.pf_fold get_current_subgoals_types lemma in (* Pp.msgnl (str "sub_gls_types1 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) let sub_gls_types = clear_goals sigma sub_gls_types in (* Pp.msgnl (str "sub_gls_types2 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) @@ -1297,9 +1297,9 @@ let is_opaque_constant c = | Declarations.Def _ -> Proof_global.Transparent | Declarations.Primitive _ -> Proof_global.Opaque -let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = +let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) - let current_proof_name = Proof_global.get_current_proof_name pstate in + let current_proof_name = Lemmas.pf_fold Proof_global.get_proof_name lemma in let name = match goal_name with | Some s -> s | None -> @@ -1323,7 +1323,7 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type let lid = ref [] in let h_num = ref (-1) in let env = Global.env () in - let pstate = build_proof env (Evd.from_env env) + let lemma = build_proof env (Evd.from_env env) ( fun gls -> let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in observe_tclTHENLIST (fun _ _ -> str "") @@ -1367,17 +1367,17 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type ) g) in - Lemmas.save_pstate_proved ~pstate ~opaque:opacity ~idopt:None + Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None in - let pstate = Lemmas.start_proof + let lemma = Lemmas.start_lemma na - (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) + Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) sigma gls_type ~hook:(Lemmas.mk_hook hook) in - let pstate = if Indfun_common.is_strict_tcc () + let lemma = if Indfun_common.is_strict_tcc () then - fst @@ by (Proofview.V82.tactic (tclIDTAC)) pstate + fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma else - fst @@ by (Proofview.V82.tactic begin + fst @@ Lemmas.by (Proofview.V82.tactic begin fun g -> tclTHEN (decompose_and_tac) @@ -1393,9 +1393,9 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type ) using_lemmas) ) tclIDTAC) - g end) pstate + g end) lemma in - if Proof_global.get_open_goals pstate = 0 then (defined pstate; None) else Some pstate + if Lemmas.(pf_fold Proof_global.get_open_goals) lemma = 0 then (defined lemma; None) else Some lemma let com_terminate interactive_proof @@ -1410,26 +1410,26 @@ let com_terminate nb_args ctx hook = let start_proof env ctx (tac_start:tactic) (tac_end:tactic) = - let pstate = Lemmas.start_proof thm_name - (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) + let lemma = Lemmas.start_lemma thm_name + (Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook in - let pstate = fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) pstate in - fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref - input_type relation rec_arg_num ))) pstate + let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) lemma in + fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref + input_type relation rec_arg_num ))) lemma in - let pstate = start_proof Global.(env ()) ctx tclIDTAC tclIDTAC in + let lemma = start_proof Global.(env ()) ctx tclIDTAC tclIDTAC in try - let sigma, new_goal_type = build_new_goal_type pstate in + let sigma, new_goal_type = build_new_goal_type lemma in let sigma = Evd.from_ctx (Evd.evar_universe_context sigma) in - open_new_goal pstate start_proof sigma + open_new_goal ~lemma start_proof sigma using_lemmas tcc_lemma_ref (Some tcc_lemma_name) (new_goal_type) with EmptySubgoals -> (* a non recursive function declared with measure ! *) tcc_lemma_ref := Not_needed; - if interactive_proof then Some pstate - else (defined pstate; None) + if interactive_proof then Some lemma + else (defined lemma; None) let start_equation (f:GlobRef.t) (term_f:GlobRef.t) (cont_tactic:Id.t list -> tactic) g = @@ -1457,9 +1457,9 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation let evd = Evd.from_ctx uctx in let f_constr = constr_of_monomorphic_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - let pstate = Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign evd + let lemma = Lemmas.start_lemma eq_name (Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd (EConstr.of_constr equation_lemma_type) in - let pstate = fst @@ by + let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (start_equation f_ref terminate_ref (fun x -> prove_eq (fun _ -> tclIDTAC) @@ -1486,14 +1486,14 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation ih = Id.of_string "______"; } ) - )) pstate in - let _ = Flags.silently (fun () -> Lemmas.save_pstate_proved ~pstate ~opaque:opacity ~idopt:None) () in + )) lemma in + let _ = Flags.silently (fun () -> Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None) () in () (* Pp.msgnl (fun _ _ -> str "eqn finished"); *) let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type_of_f r rec_arg_num eq - generate_induction_principle using_lemmas : Proof_global.t option = + generate_induction_principle using_lemmas : Lemmas.t option = let open Term in let open Constr in let open CVars in @@ -1550,8 +1550,9 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type let stop = (* XXX: What is the correct way to get sign at hook time *) let sign = Environ.named_context_val Global.(env ()) in - try com_eqn sign uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); - false + try + com_eqn sign uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); + false with e when CErrors.noncritical e -> begin if do_observe () @@ -1582,15 +1583,15 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type in (* XXX STATE Why do we need this... why is the toplevel protection not enough *) funind_purify (fun () -> - let pstate = com_terminate - interactive_proof - tcc_lemma_name - tcc_lemma_constr - is_mes functional_ref - (EConstr.of_constr rec_arg_type) - relation rec_arg_num - term_id - using_lemmas - (List.length res_vars) - evd (Lemmas.mk_hook hook) - in pstate) () + com_terminate + interactive_proof + tcc_lemma_name + tcc_lemma_constr + is_mes functional_ref + (EConstr.of_constr rec_arg_type) + relation rec_arg_num + term_id + using_lemmas + (List.length res_vars) + evd (Lemmas.mk_hook hook)) + () diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index b92ac3a0ec..e6aa452def 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -1,23 +1,21 @@ open Constr -val tclUSER_if_not_mes : +val tclUSER_if_not_mes : Tacmach.tactic -> - bool -> - Names.Id.t list option -> + bool -> + Names.Id.t list option -> Tacmach.tactic -val recursive_definition : - interactive_proof:bool -> - is_mes:bool -> - Names.Id.t -> - Constrintern.internalization_env -> - Constrexpr.constr_expr -> - Constrexpr.constr_expr -> - int -> - Constrexpr.constr_expr -> - (pconstant -> - Indfun_common.tcc_lemma_value ref -> - pconstant -> - pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> - Constrexpr.constr_expr list -> - Proof_global.t option +val recursive_definition + : interactive_proof:bool + -> is_mes:bool + -> Names.Id.t + -> Constrintern.internalization_env + -> Constrexpr.constr_expr + -> Constrexpr.constr_expr + -> int + -> Constrexpr.constr_expr + -> (pconstant -> Indfun_common.tcc_lemma_value ref -> pconstant -> + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) + -> Constrexpr.constr_expr list + -> Lemmas.t option diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 0ded60d9c7..7ba63f1830 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -336,7 +336,7 @@ let add_rewrite_hint ~poly bases ort t lcsr = let add_hints base = add_rew_rules base eqs in List.iter add_hints bases -let classify_hint _ = VtSideff [], VtLater +let classify_hint _ = VtSideff ([], VtLater) } @@ -422,7 +422,7 @@ END open Inv open Leminv -let seff id = VtSideff [id], VtLater +let seff id = VtSideff ([id], VtLater) } @@ -934,7 +934,7 @@ END VERNAC COMMAND EXTEND GrabEvars STATE proof | [ "Grab" "Existential" "Variables" ] => { classify_as_proofstep } - -> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.V82.grab_evars p) pstate } + -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.V82.grab_evars p) pstate } END (* Shelves all the goals under focus. *) @@ -966,7 +966,7 @@ END VERNAC COMMAND EXTEND Unshelve STATE proof | [ "Unshelve" ] => { classify_as_proofstep } - -> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.unshelve p) pstate } + -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.unshelve p) pstate } END (* Gives up on the goals under focus: the goals are considered solved, diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 960e5b76f8..afdea98ef5 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -376,7 +376,7 @@ let () = declare_int_option { let vernac_solve ~pstate n info tcom b = let open Goal_select in - let pstate, status = Proof_global.with_proof (fun etac p -> + let pstate, status = Proof_global.map_fold_proof_endline (fun etac p -> let with_end_tac = if b then Some etac else None in let global = match n with SelectAll | SelectList _ -> true | _ -> false in let info = Option.append info !print_info_trace in @@ -446,8 +446,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve STATE proof let solving_tac = is_explicit_terminator t in let parallel = `Yes (solving_tac,anon_abstracting_tac) in let pbr = if solving_tac then Some "par" else None in - VtProofStep{ parallel = parallel; proof_block_detection = pbr }, - VtLater + VtProofStep{ parallel = parallel; proof_block_detection = pbr } } -> { let t = rm_abstract t in vernac_solve Goal_select.SelectAll n t def @@ -494,7 +493,7 @@ END VERNAC COMMAND EXTEND VernacTacticNotation | #[ deprecation; locality; ] [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => - { VtSideff [], VtNow } -> + { VtSideff ([], VtNow) } -> { let n = Option.default 0 n in Tacentries.add_tactic_notation (Locality.make_module_locality locality) n ?deprecation r e; @@ -542,7 +541,7 @@ VERNAC COMMAND EXTEND VernacDeclareTacticDefinition | #[ deprecation; locality; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { VtSideff (List.map (function | TacticDefinition ({CAst.v=r},_) -> r - | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater + | TacticRedefinition (qid,_) -> qualid_basename qid) l, VtLater) } -> { Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l; } diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 58c8dabd79..62bc2a9259 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -83,7 +83,7 @@ open Obligations let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac -let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater) +let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[])) } diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 1a84158df7..1cc333945d 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -277,19 +277,19 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF add_setoid atts binders a aeq t n } | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] - => { VtStartProof(GuaranteesOpacity, [n]), VtLater } + => { VtStartProof(GuaranteesOpacity, [n]) } -> { if Lib.is_modtype () then CErrors.user_err Pp.(str "Add Morphism cannot be used in a module type. Use Parameter Morphism instead."); add_morphism_interactive atts m n } | #[ atts = rewrite_attributes; ] [ "Declare" "Morphism" constr(m) ":" ident(n) ] - => { VtSideff([n]), VtLater } + => { VtSideff([n], VtLater) } -> { add_morphism_as_parameter atts m n } | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => { VtStartProof(GuaranteesOpacity,[n]), VtLater } + => { VtStartProof(GuaranteesOpacity,[n]) } -> { add_morphism atts [] m s n } | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => { VtStartProof(GuaranteesOpacity,[n]), VtLater } + => { VtStartProof(GuaranteesOpacity,[n]) } -> { add_morphism atts binders m s n } END diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 7b286e69dc..2da6584aba 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -946,9 +946,9 @@ let fold_match ?(force=false) env sigma c = if dep then case_dep_scheme_kind_from_prop else case_scheme_kind_from_prop else ( - if dep - then case_dep_scheme_kind_from_type_in_prop - else case_scheme_kind_from_type) + if dep + then case_dep_scheme_kind_from_type_in_prop + else case_scheme_kind_from_type) else ((* sortc <> InProp by typing *) if dep then case_dep_scheme_kind_from_type @@ -1962,7 +1962,6 @@ let add_setoid atts binders a aeq t n = (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])] - let make_tactic name = let open Tacexpr in let tacqid = Libnames.qualid_of_string name in @@ -1988,14 +1987,14 @@ let add_morphism_as_parameter atts m n : unit = (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); declare_projection n instance_id (ConstRef cst) -let add_morphism_interactive atts m n : Proof_global.t = +let add_morphism_interactive atts m n : Lemmas.t = warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); let instance_id = add_suffix n "_Proper" in let env = Global.env () in let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in - let kind = Decl_kinds.Global, atts.polymorphic, + let kind = Decl_kinds.Global Decl_kinds.ImportDefaultBehavior, atts.polymorphic, Decl_kinds.DefinitionBody Decl_kinds.Instance in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in @@ -2010,8 +2009,8 @@ let add_morphism_interactive atts m n : Proof_global.t = let hook = Lemmas.mk_hook hook in Flags.silently (fun () -> - let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in - fst Pfedit.(by (Tacinterp.interp tac) pstate)) () + let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in + fst (Lemmas.by (Tacinterp.interp tac) lemma)) () let add_morphism atts binders m s n = init_setoid (); @@ -2023,12 +2022,12 @@ let add_morphism atts binders m s n = [cHole; s; m]) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - let _id, pstate = Classes.new_instance_interactive + let _id, lemma = Classes.new_instance_interactive ~global:atts.global atts.polymorphic instance_name binders instance_t ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in - pstate (* no instance body -> always open proof *) + lemma (* no instance body -> always open proof *) (** Bind to "rewrite" too *) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 3ef33c6dc9..a5c3782b30 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -101,16 +101,16 @@ val add_setoid -> Id.t -> unit -val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t +val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Lemmas.t val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit val add_morphism - : rewrite_attributes + : rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t - -> Proof_global.t + -> Lemmas.t val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 309db539d0..2cc6f9a279 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -12,11 +12,10 @@ open Vernacexpr open Tacexpr -open Attributes (** {5 Tactic Definitions} *) -val register_ltac : locality_flag -> ?deprecation:deprecation -> +val register_ltac : locality_flag -> ?deprecation:Deprecation.t -> Tacexpr.tacdef_body list -> unit (** Adds new Ltac definitions to the environment. *) @@ -36,7 +35,7 @@ type argument = Genarg.ArgT.any Extend.user_symbol leaves. *) val add_tactic_notation : - locality_flag -> int -> ?deprecation:deprecation -> raw_argument + locality_flag -> int -> ?deprecation:Deprecation.t -> raw_argument grammar_tactic_prod_item_expr list -> raw_tactic_expr -> unit (** [add_tactic_notation local level prods expr] adds a tactic notation in the environment at level [level] with locality [local] made of the grammar @@ -49,7 +48,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type - to finding an argument by name (as in {!Genarg}) if there is none matching. *) -val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:deprecation -> +val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:Deprecation.t -> argument grammar_tactic_prod_item_expr list list -> unit (** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND ML-side macro. *) @@ -80,7 +79,7 @@ type _ ty_sig = type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml val tactic_extend : string -> string -> level:Int.t -> - ?deprecation:deprecation -> ty_ml list -> unit + ?deprecation:Deprecation.t -> ty_ml list -> unit (** {5 ARGUMENT EXTEND} *) diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index d5f22b2c72..3347f594d2 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -55,7 +55,7 @@ type alias = KerName.t type alias_tactic = { alias_args: Id.t list; alias_body: glob_tactic_expr; - alias_deprecation: Attributes.deprecation option; + alias_deprecation: Deprecation.t option; } let alias_map = Summary.ref ~name:"tactic-alias" @@ -121,7 +121,7 @@ type ltac_entry = { tac_for_ml : bool; tac_body : glob_tactic_expr; tac_redef : ModPath.t list; - tac_deprecation : Attributes.deprecation option + tac_deprecation : Deprecation.t option } let mactab = @@ -178,7 +178,7 @@ let subst_md (subst, (local, id, b, t, deprecation)) = let classify_md (local, _, _, _, _ as o) = Substitute o let inMD : bool * ltac_constant option * bool * glob_tactic_expr * - Attributes.deprecation option -> obj = + Deprecation.t option -> obj = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 5b98daf383..2fc45760d1 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -12,7 +12,6 @@ open Names open Libnames open Tacexpr open Geninterp -open Attributes (** This module centralizes the various ways of registering tactics. *) @@ -33,7 +32,7 @@ type alias = KerName.t type alias_tactic = { alias_args: Id.t list; alias_body: glob_tactic_expr; - alias_deprecation: deprecation option; + alias_deprecation: Deprecation.t option; } (** Contents of a tactic notation *) @@ -48,7 +47,7 @@ val check_alias : alias -> bool (** {5 Coq tactic definitions} *) -val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t -> +val register_ltac : bool -> bool -> ?deprecation:Deprecation.t -> Id.t -> glob_tactic_expr -> unit (** Register a new Ltac with the given name and body. @@ -57,7 +56,7 @@ val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t -> definition. It also puts the Ltac name in the nametab, so that it can be used unqualified. *) -val redefine_ltac : bool -> ?deprecation:deprecation -> KerName.t -> +val redefine_ltac : bool -> ?deprecation:Deprecation.t -> KerName.t -> glob_tactic_expr -> unit (** Replace a Ltac with the given name and body. If the boolean flag is set to true, then this is a local redefinition. *) @@ -68,7 +67,7 @@ val interp_ltac : KerName.t -> glob_tactic_expr val is_ltac_for_ml_tactic : KerName.t -> bool (** Whether the tactic is defined from ML-side *) -val tac_deprecation : KerName.t -> deprecation option +val tac_deprecation : KerName.t -> Deprecation.t option (** The tactic deprecation notice, if any *) type ltac_entry = { @@ -78,7 +77,7 @@ type ltac_entry = { (** The current body of the tactic *) tac_redef : ModPath.t list; (** List of modules redefining the tactic in reverse chronological order *) - tac_deprecation : deprecation option; + tac_deprecation : Deprecation.t option; (** Deprecation notice to be printed when the tactic is used *) } diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index c1f7fab123..7434f81946 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -119,18 +119,13 @@ let intern_constr_reference strict ist qid = (* Internalize an isolated reference in position of tactic *) let warn_deprecated_tactic = - CWarnings.create ~name:"deprecated-tactic" ~category:"deprecated" - (fun (qid,depr) -> str "Tactic " ++ pr_qualid qid ++ - strbrk " is deprecated" ++ - pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++ - str "." ++ pr_opt (fun note -> str note) depr.Attributes.note) + Deprecation.create_warning ~object_name:"Tactic" ~warning_name:"deprecated-tactic" + pr_qualid let warn_deprecated_alias = - CWarnings.create ~name:"deprecated-tactic-notation" ~category:"deprecated" - (fun (kn,depr) -> str "Tactic Notation " ++ Pptactic.pr_alias_key kn ++ - strbrk " is deprecated since" ++ - pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++ - str "." ++ pr_opt (fun note -> str note) depr.Attributes.note) + Deprecation.create_warning ~object_name:"Tactic Notation" + ~warning_name:"deprecated-tactic-notation" + Pptactic.pr_alias_key let intern_isolated_global_tactic_reference qid = let loc = qid.CAst.loc in diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index bb53864a93..6c7b4702b6 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -194,8 +194,8 @@ let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) let mkRVar id = DAst.make @@ GRef (VarRef id,None) let mkRltacVar id = DAst.make @@ GVar (id) let mkRCast rc rt = DAst.make @@ GCast (rc, CastConv rt) -let mkRType = DAst.make @@ GSort (GType []) -let mkRProp = DAst.make @@ GSort (GProp) +let mkRType = DAst.make @@ GSort (UAnonymous {rigid=true}) +let mkRProp = DAst.make @@ GSort (UNamed [GProp,0]) let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2) let mkRConstruct c = DAst.make @@ GRef (ConstructRef c,None) let mkRInd mind = DAst.make @@ GRef (IndRef mind,None) @@ -871,8 +871,8 @@ open Constrexpr open Util (** Constructors for constr_expr *) -let mkCProp loc = CAst.make ?loc @@ CSort GProp -let mkCType loc = CAst.make ?loc @@ CSort (GType []) +let mkCProp loc = CAst.make ?loc @@ CSort (UNamed [GProp,0]) +let mkCType loc = CAst.make ?loc @@ CSort (UAnonymous {rigid=true}) let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None) let rec mkCHoles ?loc n = if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index dbb0f25abf..91905d277c 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -336,14 +336,14 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ let sigma, p = (* The resulting goal *) Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in - let elim, gl = + let elim, gl = let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in let sort = elimination_sort_of_goal gl in let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in if dir = R2L then elim, gl else (* taken from Coq's rewrite *) let elim, _ = destConst elim in let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in - let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in + let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in mkConst c1', gl in let elim = EConstr.of_constr elim in |