[declare] Refactor constant information into a record.

dev/base_include

@@ -111,10 +111,8 @@ open Search
 open Evar_refiner
 open Goal
 open Logic
-open Pfedit
 open Proof
 open Proof_using
-open Proof_global
 open Redexpr
 open Refiner
 open Tacmach

dev/ci/user-overlays/12372-ejgallego-proof+info.sh

@@ -0,0 +1,24 @@
+if [ "$CI_PULL_REQUEST" = "12372" ] || [ "$CI_BRANCH" = "proof+info" ]; then
+
+    rewriter_CI_REF=proof+info
+    rewriter_CI_GITURL=https://github.com/ejgallego/rewriter
+
+    paramcoq_CI_REF=proof+info
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+    mtac2_CI_REF=proof+info
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+    equations_CI_REF=proof+info
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    elpi_CI_REF=proof+info
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    aac_tactics_CI_REF=proof+info
+    aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics
+
+    metacoq_CI_REF=proof+info
+    metacoq_CI_GITURL=https://github.com/ejgallego/metacoq
+
+fi

doc/plugin_tutorial/tuto1/src/g_tuto1.mlg

@@ -286,8 +286,8 @@ END
 VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
 | ![ proof_query ] [ "ExploreProof" ] ->
   { fun ~pstate ->
-    let sigma, env = Declare.get_current_context pstate in
-    let pprf = Proof.partial_proof (Declare.Proof.get_proof pstate) in
+    let sigma, env = Declare.Proof.get_current_context pstate in
+    let pprf = Proof.partial_proof (Declare.Proof.get pstate) in
     Feedback.msg_notice
       (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
   }

doc/plugin_tutorial/tuto1/src/simple_declare.ml

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

ide/coqide/idetop.ml

@@ -343,7 +343,7 @@ let search flags =
   let pstate = Vernacstate.Declare.get_pstate () in
   let sigma, env = match pstate with
   | None -> let env = Global.env () in Evd.(from_env env, env)
-  | Some p -> Declare.get_goal_context p 1 in
+  | Some p -> Declare.Proof.get_goal_context p 1 in
   List.map export_coq_object (Search.interface_search env sigma (
     List.map (fun (c, b) -> (import_search_constraint c, b)) flags)
   )

plugins/derive/derive.ml

@@ -15,7 +15,7 @@ open Context.Named.Declaration
     (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 name : Lemmas.t =
+let start_deriving f suchthat name : Declare.Proof.t =
 
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -40,8 +40,7 @@ let start_deriving f suchthat name : Lemmas.t =
                 TNil sigma))))))
   in
 
-  let info = Lemmas.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
-  let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in
-  Lemmas.pf_map (Declare.Proof.map_proof begin fun p ->
-    Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
-  end) lemma
+  let info = Declare.Info.make ~poly ~kind () in
+  let lemma = Declare.Proof.start_derive ~name ~f ~info goals in
+  Declare.Proof.map lemma ~f:(fun p ->
+      Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)

plugins/derive/derive.mli

@@ -16,4 +16,4 @@ val start_deriving
   :  Names.Id.t
   -> Constrexpr.constr_expr
   -> Names.Id.t
-  -> Lemmas.t
+  -> Declare.Proof.t

plugins/extraction/extract_env.ml

@@ -729,13 +729,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 = Declare.Proof.get_proof pstate in
-  let sigma, env = Declare.get_current_context pstate in
+  let prf = Declare.Proof.get pstate in
+  let sigma, env = Declare.Proof.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 (Declare.Proof.get_proof_name pstate) in
+    let l = Label.of_id (Declare.Proof.get_name pstate) in
     let fake_ref = GlobRef.ConstRef (Constant.make2 mp l) in
     let decl = Dterm (fake_ref, ast, ty) in
     print_one_decl [] mp decl

plugins/funind/functional_principles_proofs.ml

@@ -853,12 +853,16 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
 
   (*i The next call to mk_equation_id is valid since we are
      constructing the lemma Ensures by: obvious i*)
-  let lemma =
-    Lemmas.start_lemma ~name:(mk_equation_id f_id) ~poly:false evd lemma_type
+  let info = Declare.Info.make () in
+  let cinfo =
+    Declare.CInfo.make ~name:(mk_equation_id f_id) ~typ:lemma_type ()
+  in
+  let lemma = Declare.Proof.start ~cinfo ~info evd in
+  let lemma, _ =
+    Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
   in
-  let lemma, _ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in
-  let () =
-    Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None
+  let (_ : _ list) =
+    Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
   in
   evd
 

plugins/funind/gen_principle.ml

@@ -319,7 +319,7 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts
     let entry = Declare.definition_entry ~univs ?types body in
     let (_ : Names.GlobRef.t) =
       Declare.declare_entry ~name:new_princ_name ~hook
-        ~scope:(Declare.Global Declare.ImportDefaultBehavior)
+        ~scope:(Locality.Global Locality.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:(Declare.Global Declare.ImportDefaultBehavior)
+      ~scope:(Locality.Global Locality.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:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false
+      ~scope:(Locality.Global Locality.ImportDefaultBehavior) ~poly:false
       fixpoint_exprl;
     let evd, rev_pconstants =
       List.fold_left
@@ -1370,12 +1370,12 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list =
       | None -> raise Not_found
       | Some finfos -> finfos
     in
-    let open Declare in
     match finfos.equation_lemma with
-    | None -> Transparent (* non recursive definition *)
+    | None -> Vernacexpr.Transparent (* non recursive definition *)
     | Some equation ->
-      if Declareops.is_opaque (Global.lookup_constant equation) then Opaque
-      else Transparent
+      if Declareops.is_opaque (Global.lookup_constant equation) then
+        Vernacexpr.Opaque
+      else Vernacexpr.Transparent
   in
   let body, typ, univs, _hook, sigma0 =
     try
@@ -1518,12 +1518,14 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
             i*)
           let lem_id = mk_correct_id f_id in
           let typ, _ = lemmas_types_infos.(i) in
-          let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false !evd typ in
+          let info = Declare.Info.make () in
+          let cinfo = Declare.CInfo.make ~name:lem_id ~typ () in
+          let lemma = Declare.Proof.start ~cinfo ~info !evd in
           let lemma =
-            fst @@ Lemmas.by (Proofview.V82.tactic (proving_tac i)) lemma
+            fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
-          let () =
-            Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent
+          let (_ : GlobRef.t list) =
+            Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
               ~idopt:None
           in
           let finfo =
@@ -1580,21 +1582,22 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
               Ensures by: obvious
             i*)
           let lem_id = mk_complete_id f_id in
-          let lemma =
-            Lemmas.start_lemma ~name:lem_id ~poly:false sigma
-              (fst lemmas_types_infos.(i))
+          let info = Declare.Info.make () in
+          let cinfo =
+            Declare.CInfo.make ~name:lem_id ~typ:(fst lemmas_types_infos.(i)) ()
           in
+          let lemma = Declare.Proof.start ~cinfo sigma ~info in
           let lemma =
             fst
-              (Lemmas.by
+              (Declare.Proof.by
                  (Proofview.V82.tactic
                     (observe_tac
                        ("prove completeness (" ^ Id.to_string f_id ^ ")")
                        (proving_tac i)))
                  lemma)
           in
-          let () =
-            Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent
+          let (_ : _ list) =
+            Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
               ~idopt:None
           in
           let finfo =
@@ -1769,7 +1772,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt
     using_lemmas args ret_type body
 
 let do_generate_principle_aux pconstants on_error register_built
-    interactive_proof fixpoint_exprl : Lemmas.t option =
+    interactive_proof fixpoint_exprl : Declare.Proof.t option =
   List.iter
     (fun {Vernacexpr.notations} ->
       if not (List.is_empty notations) then
@@ -2155,7 +2158,7 @@ let make_graph (f_ref : GlobRef.t) =
 
 (* *************** statically typed entrypoints ************************* *)
 
-let do_generate_principle_interactive fixl : Lemmas.t =
+let do_generate_principle_interactive fixl : Declare.Proof.t =
   match do_generate_principle_aux [] warning_error true true fixl with
   | Some lemma -> lemma
   | None ->
@@ -2199,7 +2202,7 @@ let build_scheme fas =
   List.iter2
     (fun (princ_id, _, _) (body, types, univs, opaque) ->
       let (_ : Constant.t) =
-        let opaque = if opaque = Declare.Opaque then true else false in
+        let opaque = if opaque = Vernacexpr.Opaque then true else false in
         let def_entry = Declare.definition_entry ~univs ~opaque ?types body in
         Declare.declare_constant ~name:princ_id
           ~kind:Decls.(IsProof Theorem)

plugins/funind/gen_principle.mli

@@ -12,7 +12,7 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 
 val do_generate_principle_interactive :
-  Vernacexpr.fixpoint_expr list -> Lemmas.t
+  Vernacexpr.fixpoint_expr list -> Declare.Proof.t
 
 val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit
 val make_graph : Names.GlobRef.t -> unit