Merge PR #12241: [declare] Merge DeclareDef into Declare

Reviewed-by: Matafou
Reviewed-by: SkySkimmer

doc/plugin_tutorial/tuto1/src/simple_declare.ml

@@ -1,6 +1,6 @@
 let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
-  let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
+  let scope = Declare.Global Declare.ImportDefaultBehavior in
   let kind = Decls.(IsDefinition Definition) in
-  DeclareDef.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl
+  Declare.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl
     ~opaque:false ~poly ~types:None ~body sigma

plugins/funind/gen_principle.ml

@@ -218,7 +218,7 @@ let build_functional_principle (sigma : Evd.evar_map) old_princ_type sorts funs
     Declare.build_by_tactic env ~uctx ~poly:false ~typ ftac
   in
   (* uctx was ignored before *)
-  let hook = DeclareDef.Hook.make (hook new_principle_type) in
+  let hook = Declare.Hook.make (hook new_principle_type) in
   (body, typ, univs, hook, sigma)
 
 let change_property_sort evd toSort princ princName =
@@ -318,8 +318,8 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts
     let uctx = Evd.evar_universe_context sigma in
     let entry = Declare.definition_entry ~univs ?types body in
     let (_ : Names.GlobRef.t) =
-      DeclareDef.declare_entry ~name:new_princ_name ~hook
-        ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+      Declare.declare_entry ~name:new_princ_name ~hook
+        ~scope:(Declare.Global Declare.ImportDefaultBehavior)
         ~kind:Decls.(IsProof Theorem)
         ~impargs:[] ~uctx entry
     in
@@ -400,7 +400,7 @@ let register_struct is_rec fixpoint_exprl =
           Pp.(str "Body of Function must be given")
     in
     ComDefinition.do_definition ~name:fname.CAst.v ~poly:false
-      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+      ~scope:(Declare.Global Declare.ImportDefaultBehavior)
       ~kind:Decls.Definition univs binders None body (Some rtype);
     let evd, rev_pconstants =
       List.fold_left
@@ -419,7 +419,7 @@ let register_struct is_rec fixpoint_exprl =
     (None, evd, List.rev rev_pconstants)
   | _ ->
     ComFixpoint.do_fixpoint
-      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false
+      ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false
       fixpoint_exprl;
     let evd, rev_pconstants =
       List.fold_left

plugins/funind/recdef.ml

@@ -1483,7 +1483,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
     let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
     Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None
   in
-  let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in
+  let info = Lemmas.Info.make ~hook:(Declare.Hook.make hook) () in
   let lemma =
     Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type
   in
@@ -1721,7 +1721,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
   let tcc_lemma_name = add_suffix function_name "_tcc" in
   let tcc_lemma_constr = ref Undefined in
   (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
-  let hook {DeclareDef.Hook.S.uctx; _} =
+  let hook {Declare.Hook.S.uctx; _} =
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref =
       declare_f function_name Decls.(IsProof Lemma) arg_types term_ref
@@ -1767,5 +1767,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
         functional_ref
         (EConstr.of_constr rec_arg_type)
         relation rec_arg_num term_id using_lemmas (List.length res_vars) evd
-        (DeclareDef.Hook.make hook))
+        (Declare.Hook.make hook))
     ()

plugins/ltac/g_ltac.mlg

@@ -342,7 +342,7 @@ GRAMMAR EXTEND Gram
   hint:
     [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
         tac = Pltac.tactic ->
-        { ComHints.HintsExtern (n,c, in_tac tac) } ] ]
+        { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ]
   ;
   operconstr: LEVEL "0"
     [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->

plugins/ltac/rewrite.ml

@@ -1894,10 +1894,10 @@ let declare_projection name instance_id r =
     in it_mkProd_or_LetIn ccl ctx
   in
   let types = Some (it_mkProd_or_LetIn typ ctx) in
-  let kind, opaque, scope = Decls.(IsDefinition Definition), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+  let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
   let _r : GlobRef.t =
-    DeclareDef.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
+    Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
   in ()
 
 let build_morphism_signature env sigma m =
@@ -1961,10 +1961,10 @@ let add_morphism_as_parameter atts m n : unit =
   let env = Global.env () in
   let evd = Evd.from_env env in
   let poly = atts.polymorphic in
-  let kind, opaque, scope = Decls.(IsAssumption Logical), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+  let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
   let evd, types = build_morphism_signature env evd m in
-  let evd, pe = DeclareDef.prepare_parameter ~poly ~udecl ~types evd in
+  let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in
   let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in
   let cst = GlobRef.ConstRef cst in
   Classes.add_instance
@@ -1981,15 +1981,15 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let poly = atts.polymorphic in
   let kind = Decls.(IsDefinition Instance) in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
-  let hook { DeclareDef.Hook.S.dref; _ } = dref |> function
+  let hook { Declare.Hook.S.dref; _ } = dref |> function
     | GlobRef.ConstRef cst ->
       Classes.add_instance (Classes.mk_instance
                       (PropGlobal.proper_class env evd) Hints.empty_hint_info
                       atts.global (GlobRef.ConstRef cst));
       declare_projection n instance_id (GlobRef.ConstRef cst)
     | _ -> assert false
   in
-  let hook = DeclareDef.Hook.make hook in
+  let hook = Declare.Hook.make hook in
   let info = Lemmas.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->

vernac/classes.ml

@@ -313,8 +313,8 @@ let instance_hook info global ?hook cst =
 
 let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype =
   let kind = Decls.(IsDefinition Instance) in
-  let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
-  let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs
+  let scope = Declare.Global Declare.ImportDefaultBehavior in
+  let kn = Declare.declare_definition ~name ~kind ~scope ~impargs
       ~opaque:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in
   instance_hook info global ?hook kn
 
@@ -325,7 +325,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst
   in
   let (_, ty_constr) = instance_constructor (k,u) subst in
   let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-  let sigma, entry = DeclareDef.prepare_parameter ~poly sigma ~udecl ~types:termtype in
+  let sigma, entry = Declare.prepare_parameter ~poly sigma ~udecl ~types:termtype in
   let cst = Declare.declare_constant ~name
       ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in
   DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma);
@@ -334,17 +334,17 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst
   instance_hook pri global cst
 
 let declare_instance_program env sigma ~global ~poly name pri impargs udecl term termtype =
-  let hook { DeclareDef.Hook.S.scope; dref; _ } =
+  let hook { Declare.Hook.S.scope; dref; _ } =
     let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in
     let pri = intern_info pri in
     let env = Global.env () in
     let sigma = Evd.from_env env in
     declare_instance env sigma (Some pri) (not global) (GlobRef.ConstRef cst)
   in
   let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in
-  let hook = DeclareDef.Hook.make hook in
+  let hook = Declare.Hook.make hook in
   let uctx = Evd.evar_universe_context sigma in
-  let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in
+  let scope, kind = Declare.Global Declare.ImportDefaultBehavior, Decls.Instance in
   let _ : DeclareObl.progress =
     Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls
   in ()
@@ -357,7 +357,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id
   let gls = List.rev (Evd.future_goals sigma) in
   let sigma = Evd.reset_future_goals sigma in
   let kind = Decls.(IsDefinition Instance) in
-  let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in
+  let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in
   let info = Lemmas.Info.make ~hook ~kind () in
   (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails!
      This is due to a bug in proof_global :( *)

vernac/classes.mli

@@ -22,7 +22,7 @@ val declare_instance : ?warn:bool -> env -> Evd.evar_map ->
     Does nothing — or emit a “not-a-class” warning if the [warn] argument is set —
     when said type is not a registered type class. *)
 
-val existing_instance : bool -> qualid -> ComHints.hint_info_expr option -> unit
+val existing_instance : bool -> qualid -> Vernacexpr.hint_info_expr option -> unit
 (** globality, reference, optional priority and pattern information *)
 
 val new_instance_interactive
@@ -34,7 +34,7 @@ val new_instance_interactive
   -> ?generalize:bool
   -> ?tac:unit Proofview.tactic
   -> ?hook:(GlobRef.t -> unit)
-  -> ComHints.hint_info_expr
+  -> Vernacexpr.hint_info_expr
   -> (bool * constr_expr) option
   -> Id.t * Lemmas.t
 
@@ -47,7 +47,7 @@ val new_instance
   -> (bool * constr_expr)
   -> ?generalize:bool
   -> ?hook:(GlobRef.t -> unit)
-  -> ComHints.hint_info_expr
+  -> Vernacexpr.hint_info_expr
   -> Id.t
 
 val new_instance_program
@@ -59,7 +59,7 @@ val new_instance_program
   -> (bool * constr_expr) option
   -> ?generalize:bool
   -> ?hook:(GlobRef.t -> unit)
-  -> ComHints.hint_info_expr
+  -> Vernacexpr.hint_info_expr
   -> Id.t
 
 val declare_new_instance
@@ -69,7 +69,7 @@ val declare_new_instance
   -> ident_decl
   -> local_binder_expr list
   -> constr_expr
-  -> ComHints.hint_info_expr
+  -> Vernacexpr.hint_info_expr
   -> unit
 
 (** {6 Low level interface used by Add Morphism, do not use } *)

vernac/comAssumption.ml

@@ -87,8 +87,7 @@ let context_set_of_entry = function
   | Monomorphic_entry uctx -> uctx
 
 let declare_assumptions ~poly ~scope ~kind univs nl l =
-  let open DeclareDef in
-  let () = match scope with
+  let () = let open Declare in match scope with
     | Discharge ->
       (* declare universes separately for variables *)
       DeclareUctx.declare_universe_context ~poly (context_set_of_entry (fst univs))
@@ -100,10 +99,10 @@ let declare_assumptions ~poly ~scope ~kind univs nl l =
       let univs,subst' =
         List.fold_left_map (fun univs id ->
             let refu = match scope with
-              | Discharge ->
+              | Declare.Discharge ->
                 declare_variable is_coe ~kind typ imps Glob_term.Explicit id;
                 GlobRef.VarRef id.CAst.v, Univ.Instance.empty
-              | Global local ->
+              | Declare.Global local ->
                 declare_axiom is_coe ~local ~poly ~kind typ univs imps nl id
             in
             next_univs univs, (id.CAst.v, Constr.mkRef refu))
@@ -130,7 +129,7 @@ let process_assumptions_udecls ~scope l =
       udecl, id
     | (_, ([], _))::_ | [] -> assert false
   in
-  let open DeclareDef in
+  let open Declare in
   let () = match scope, udecl with
     | Discharge, Some _ ->
       let loc = first_id.CAst.loc in
@@ -208,7 +207,7 @@ let context_insection sigma ~poly ctx =
         let uctx = Evd.evar_universe_context sigma in
         let kind = Decls.(IsDefinition Definition) in
         let _ : GlobRef.t =
-          DeclareDef.declare_entry ~name ~scope:DeclareDef.Discharge
+          Declare.declare_entry ~name ~scope:Declare.Discharge
             ~kind ~impargs:[] ~uctx entry
         in
         ()

vernac/comAssumption.mli

@@ -17,7 +17,7 @@ open Constrexpr
 val do_assumptions
   :  program_mode:bool
   -> poly:bool
-  -> scope:DeclareDef.locality
+  -> scope:Declare.locality
   -> kind:Decls.assumption_object_kind
   -> Declaremods.inline
   -> (ident_decl list * constr_expr) with_coercion list

vernac/comCoercion.ml

@@ -352,8 +352,8 @@ let try_add_new_identity_coercion id ~local ~poly ~source ~target =
 let try_add_new_coercion_with_source ref ~local ~poly ~source =
   try_add_new_coercion_core ref ~local poly (Some source) None false
 
-let add_coercion_hook poly { DeclareDef.Hook.S.scope; dref; _ } =
-  let open DeclareDef in
+let add_coercion_hook poly { Declare.Hook.S.scope; dref; _ } =
+  let open Declare in
   let local = match scope with
   | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *)
   | Global ImportNeedQualified -> true
@@ -363,10 +363,10 @@ let add_coercion_hook poly { DeclareDef.Hook.S.scope; dref; _ } =
   let msg = Nametab.pr_global_env Id.Set.empty dref ++ str " is now a coercion" in
   Flags.if_verbose Feedback.msg_info msg
 
-let add_coercion_hook ~poly = DeclareDef.Hook.make (add_coercion_hook poly)
+let add_coercion_hook ~poly = Declare.Hook.make (add_coercion_hook poly)
 
-let add_subclass_hook ~poly { DeclareDef.Hook.S.scope; dref; _ } =
-  let open DeclareDef in
+let add_subclass_hook ~poly { Declare.Hook.S.scope; dref; _ } =
+  let open Declare in
   let stre = match scope with
   | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *)
   | Global ImportNeedQualified -> true
@@ -375,4 +375,4 @@ let add_subclass_hook ~poly { DeclareDef.Hook.S.scope; dref; _ } =
   let cl = class_of_global dref in
   try_add_new_coercion_subclass cl ~local:stre ~poly
 
-let add_subclass_hook ~poly = DeclareDef.Hook.make (add_subclass_hook ~poly)
+let add_subclass_hook ~poly = Declare.Hook.make (add_subclass_hook ~poly)

vernac/comCoercion.mli

@@ -46,8 +46,8 @@ val try_add_new_identity_coercion
   -> local:bool
   -> poly:bool -> source:cl_typ -> target:cl_typ -> unit
 
-val add_coercion_hook : poly:bool -> DeclareDef.Hook.t
+val add_coercion_hook : poly:bool -> Declare.Hook.t
 
-val add_subclass_hook : poly:bool -> DeclareDef.Hook.t
+val add_subclass_hook : poly:bool -> Declare.Hook.t
 
 val class_of_global : GlobRef.t -> cl_typ

vernac/comDefinition.ml

@@ -117,7 +117,7 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
   in
   let kind = Decls.IsDefinition kind in
   let _ : Names.GlobRef.t =
-    DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs
+    Declare.declare_definition ~name ~scope ~kind ?hook ~impargs
       ~opaque:false ~poly evd ~udecl ~types ~body
   in ()
 
@@ -126,7 +126,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c
   let (body, types), evd, udecl, impargs =
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
-  let term, ty, uctx, obls = DeclareDef.prepare_obligation ~name ~poly ~body ~types ~udecl evd in
+  let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in
   let _ : DeclareObl.progress =
     Obligations.add_definition
       ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls

vernac/comDefinition.mli

@@ -15,9 +15,9 @@ open Constrexpr
 (** {6 Definitions/Let} *)
 
 val do_definition
-  :  ?hook:DeclareDef.Hook.t
+  :  ?hook:Declare.Hook.t
   -> name:Id.t
-  -> scope:DeclareDef.locality
+  -> scope:Declare.locality
   -> poly:bool
   -> kind:Decls.definition_object_kind
   -> universe_decl_expr option
@@ -28,9 +28,9 @@ val do_definition
   -> unit
 
 val do_definition_program
-  :  ?hook:DeclareDef.Hook.t
+  :  ?hook:Declare.Hook.t
   -> name:Id.t
-  -> scope:DeclareDef.locality
+  -> scope:Declare.locality
   -> poly:bool
   -> kind:Decls.definition_object_kind
   -> universe_decl_expr option

vernac/comFixpoint.ml

@@ -257,7 +257,7 @@ let build_recthms ~indexes fixnames fixtypes fiximps =
   in
   let thms =
     List.map3 (fun name typ (ctx,impargs,_) ->
-        { DeclareDef.Recthm.name
+        { Declare.Recthm.name
         ; typ
         ; args = List.map Context.Rel.Declaration.get_name ctx
         ; impargs})
@@ -284,7 +284,7 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
   let fix_kind = Decls.IsDefinition fix_kind in
   let _ : GlobRef.t list =
-    DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx
+    Declare.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx
       ~possible_indexes:indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration
       fixitems
   in

vernac/comFixpoint.mli

@@ -16,16 +16,16 @@ open Vernacexpr
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint_interactive :
-  scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t
+  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t
 
 val do_fixpoint :
-  scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit
+  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit
 
 val do_cofixpoint_interactive :
-  scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t
+  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t
 
 val do_cofixpoint :
-  scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit
+  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit
 
 (************************************************************************)
 (** Internal API  *)