From 17ba18d81e5fe3dc153b1c12ac1b8daeb5474d48 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 2 May 2019 06:10:29 +0200
Subject: [lemmas] Turn Lemmas.info into a proper type with constructor.

Lemmas.info was a bit out of hand, as well as the parameters to the
`start_*` family. Most of the info is not needed and should hopefully
remain constrained to special cases, most callers only set the hook,
and obligations should be better served by a `start_obligation`
function soon.
---
 plugins/derive/derive.ml                       |  4 ++--
 plugins/funind/functional_principles_proofs.ml |  9 +++++----
 plugins/funind/functional_principles_types.ml  |  5 ++---
 plugins/funind/invfun.ml                       | 12 ++++++------
 plugins/funind/recdef.ml                       | 19 ++++++++++++-------
 plugins/ltac/rewrite.ml                        |  3 ++-
 6 files changed, 29 insertions(+), 23 deletions(-)

(limited to 'plugins')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 72ca5dc8c4..22e20e2c52 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -39,8 +39,8 @@ let start_deriving f suchthat name : Lemmas.t =
                 TNil sigma))))))
   in
 
-  let proof_ending = Lemmas.Proof_ending.(End_derive {f; name}) in
-  let lemma = Lemmas.start_dependent_lemma name kind goals ~proof_ending in
+  let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) () in
+  let lemma = Lemmas.start_dependent_lemma ~name ~kind ~info goals 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/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ce3b5a82d6..9c593a55d8 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -994,10 +994,11 @@ 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*)
-    (mk_equation_id f_id)
-    Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem)
-    evd
-  lemma_type
+      ~name:(mk_equation_id f_id)
+      ~kind:Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem)
+
+      evd
+      lemma_type
   in
   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
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d49d657d38..1154198d43 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -308,9 +308,8 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   evd := sigma;
   let hook = DeclareDef.Hook.make (hook new_principle_type) in
   let lemma =
-    Lemmas.start_lemma
-      new_princ_name
-      Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
+    Lemmas.start_lemma ~name:new_princ_name
+      ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
       !evd
       (EConstr.of_constr new_principle_type)
   in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2020881c7c..48b5e56635 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -804,10 +804,10 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let lem_id = mk_correct_id f_id in
          let (typ,_) = lemmas_types_infos.(i) in
          let lemma = Lemmas.start_lemma
-           lem_id
-           Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
-           !evd
-           typ in
+             ~name:lem_id
+             ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
+             !evd
+             typ in
          let lemma = fst @@ Lemmas.by
                    (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
                                                       (proving_tac i))) lemma in
@@ -865,8 +865,8 @@ 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 lemma = Lemmas.start_lemma lem_id
-           Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma
+         let lemma = Lemmas.start_lemma ~name:lem_id
+           ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma
          (fst lemmas_types_infos.(i)) in
          let lemma = fst (Lemmas.by
            (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 2647e7449b..c97b39ff79 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1367,10 +1367,11 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
     in
     Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None
   in
+  let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in
   let lemma = Lemmas.start_lemma
-    na
-    Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
-    sigma gls_type ~hook:(DeclareDef.Hook.make hook) in
+      ~name:na
+      ~kind:Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~info
+      sigma gls_type in
   let lemma = if Indfun_common.is_strict_tcc  ()
   then
     fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma
@@ -1408,9 +1409,13 @@ let com_terminate
     nb_args ctx
     hook =
   let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
-    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 info = Lemmas.Info.make ~hook () in
+    let lemma = Lemmas.start_lemma ~name:thm_name
+        ~kind:(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
+        ~sign:(Environ.named_context_val env)
+        ~info
+        ctx
+        (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) in
     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
@@ -1455,7 +1460,7 @@ 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 lemma = Lemmas.start_lemma eq_name (Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd
+    let lemma = Lemmas.start_lemma ~name:eq_name ~kind:(Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd
        (EConstr.of_constr equation_lemma_type) in
     let lemma = fst @@ Lemmas.by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index f977ba34d2..49265802ae 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2007,9 +2007,10 @@ let add_morphism_interactive atts m n : Lemmas.t =
     | _ -> assert false
   in
   let hook = DeclareDef.Hook.make hook in
+  let info = Lemmas.Info.make ~hook () in
   Flags.silently
     (fun () ->
-       let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+       let lemma = Lemmas.start_lemma ~name:instance_id ~kind ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
        fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
-- 
cgit v1.2.3


From fd2d2a8178d78e441fb3191cf112ed517dc791af Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 May 2019 05:33:10 +0200
Subject: [proof] Remove duplicated universe polymorphic from decl_kinds

This information is already present on `Proof.t`, so we extract it
form there.

Moreover, this information is essential to the lower-level proof, as
opposed to the "kind" information which is only relevant to the vernac
layer; we will move it thus to its proper layer in subsequent commits.
---
 plugins/derive/derive.ml                       | 5 +++--
 plugins/funind/functional_principles_proofs.ml | 4 ++--
 plugins/funind/functional_principles_types.ml  | 6 ++++--
 plugins/funind/indfun_common.ml                | 2 +-
 plugins/funind/invfun.ml                       | 8 +++++---
 plugins/funind/recdef.ml                       | 8 +++++---
 plugins/ltac/rewrite.ml                        | 5 +++--
 7 files changed, 23 insertions(+), 15 deletions(-)

(limited to 'plugins')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 22e20e2c52..8c2cf3c553 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -19,7 +19,8 @@ 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 ImportDefaultBehavior,false,DefinitionBody Definition) in
+  let poly = false in
+  let kind = Decl_kinds.(Global ImportDefaultBehavior,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
@@ -40,7 +41,7 @@ let start_deriving f suchthat name : Lemmas.t =
   in
 
   let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) () in
-  let lemma = Lemmas.start_dependent_lemma ~name ~kind ~info goals in
+  let lemma = Lemmas.start_dependent_lemma ~name ~poly ~kind ~info goals 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/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 9c593a55d8..c37e6f7402 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -995,8 +995,8 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
       Ensures by: obvious
       i*)
       ~name:(mk_equation_id f_id)
-      ~kind:Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem)
-
+      ~poly:false
+      ~kind:(Decl_kinds.(Global ImportDefaultBehavior, Proof Theorem))
       evd
       lemma_type
   in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1154198d43..1b447bd26a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -308,8 +308,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   evd := sigma;
   let hook = DeclareDef.Hook.make (hook new_principle_type) in
   let lemma =
-    Lemmas.start_lemma ~name:new_princ_name
-      ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
+    Lemmas.start_lemma
+      ~name:new_princ_name
+      ~poly:false
+      ~kind:(Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem))
       !evd
       (EConstr.of_constr new_principle_type)
   in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 17c79e0e6c..a5a07934ac 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -123,7 +123,7 @@ open Declare
 
 let definition_message = Declare.definition_message
 
-let save id const ?hook uctx (locality,_,kind) =
+let save id const ?hook uctx (locality,kind) =
   let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
   let r = match locality with
     | Discharge ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 48b5e56635..e5b0a5d032 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -805,7 +805,8 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let (typ,_) = lemmas_types_infos.(i) in
          let lemma = Lemmas.start_lemma
              ~name:lem_id
-             ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
+             ~poly:false
+             ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem)
              !evd
              typ in
          let lemma = fst @@ Lemmas.by
@@ -866,8 +867,9 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
            i*)
          let lem_id = mk_complete_id f_id in
          let lemma = Lemmas.start_lemma ~name:lem_id
-           ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma
-         (fst lemmas_types_infos.(i)) in
+             ~poly:false
+             ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem) sigma
+             (fst lemmas_types_infos.(i)) in
          let lemma = fst (Lemmas.by
            (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
               (proving_tac i))) lemma) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c97b39ff79..187d907dc5 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1370,7 +1370,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
   let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in
   let lemma = Lemmas.start_lemma
       ~name:na
-      ~kind:Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~info
+      ~poly:false (* FIXME *)
+      ~kind:Decl_kinds.(Global ImportDefaultBehavior, Proof Lemma) ~info
       sigma gls_type in
   let lemma = if Indfun_common.is_strict_tcc  ()
   then
@@ -1411,7 +1412,8 @@ let com_terminate
   let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
     let info = Lemmas.Info.make ~hook () in
     let lemma = Lemmas.start_lemma ~name:thm_name
-        ~kind:(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
+        ~poly:false (*FIXME*)
+        ~kind:(Global ImportDefaultBehavior, Proof Lemma)
         ~sign:(Environ.named_context_val env)
         ~info
         ctx
@@ -1460,7 +1462,7 @@ 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 lemma = Lemmas.start_lemma ~name:eq_name ~kind:(Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd
+    let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~kind:(Global ImportDefaultBehavior, Proof Lemma) ~sign evd
        (EConstr.of_constr equation_lemma_type) in
     let lemma = fst @@ Lemmas.by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 49265802ae..d87b7a1770 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1994,7 +1994,8 @@ let add_morphism_interactive atts m n : Lemmas.t =
   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 Decl_kinds.ImportDefaultBehavior, atts.polymorphic,
+  let poly = atts.polymorphic in
+  let kind = Decl_kinds.(Global ImportDefaultBehavior),
              Decl_kinds.DefinitionBody Decl_kinds.Instance
   in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
@@ -2010,7 +2011,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let info = Lemmas.Info.make ~hook () in
   Flags.silently
     (fun () ->
-       let lemma = Lemmas.start_lemma ~name:instance_id ~kind ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+       let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~kind ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
        fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
-- 
cgit v1.2.3


From 8b903319eae4d645f9385e8280d04d18a4f3a2bc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Jun 2019 06:09:24 +0200
Subject: [lemmas] [proof] Split proof kinds into per-layer components.

We split `{goal,declaration,assumption}_kind` into their
components. This makes sense as each part of this triple is handled by
a different layer, namely:

- `polymorphic` status: necessary for the lower engine layers;
- `locality`: only used in `vernac` top-level constants
- `kind`: merely used for cosmetic purposes [could indeed be removed /
  pushed upwards]

We also profit from this refactoring to add some named parameters to
the top-level definition API which is quite parameter-hungry.

More refactoring is possible and will come in further commits, in
particular this is a step towards unifying the definition / lemma save path.
---
 plugins/derive/derive.ml                       |  6 +++---
 plugins/funind/functional_principles_proofs.ml |  6 +++++-
 plugins/funind/functional_principles_types.ml  | 19 +++++++++----------
 plugins/funind/indfun.ml                       |  8 +++++---
 plugins/funind/indfun_common.ml                |  2 +-
 plugins/funind/indfun_common.mli               |  3 ++-
 plugins/funind/invfun.ml                       | 18 +++++++++++-------
 plugins/funind/recdef.ml                       | 12 ++++++------
 plugins/ltac/rewrite.ml                        |  8 +++-----
 9 files changed, 45 insertions(+), 37 deletions(-)

(limited to 'plugins')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 8c2cf3c553..e34150f2b3 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -20,7 +20,7 @@ let start_deriving f suchthat name : Lemmas.t =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let poly = false in
-  let kind = Decl_kinds.(Global ImportDefaultBehavior,DefinitionBody Definition) in
+  let kind = Decl_kinds.(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
@@ -40,8 +40,8 @@ let start_deriving f suchthat name : Lemmas.t =
                 TNil sigma))))))
   in
 
-  let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) () in
-  let lemma = Lemmas.start_dependent_lemma ~name ~poly ~kind ~info goals in
+  let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) ~kind () in
+  let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals 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/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c37e6f7402..0d3c7b365f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -990,13 +990,17 @@ 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 info = Lemmas.Info.make
+      ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+      ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
+
   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*)
       ~name:(mk_equation_id f_id)
       ~poly:false
-      ~kind:(Decl_kinds.(Global ImportDefaultBehavior, Proof Theorem))
+      ~info
       evd
       lemma_type
   in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1b447bd26a..65b114fc03 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -311,7 +311,6 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
     Lemmas.start_lemma
       ~name:new_princ_name
       ~poly:false
-      ~kind:(Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem))
       !evd
       (EConstr.of_constr new_principle_type)
   in
@@ -325,10 +324,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   (*    end; *)
 
   let open Proof_global in
-  let { id; entries; persistence } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+  let { id; entries } = 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
+    id, entry, hook
   | _ ->
     CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
 
@@ -380,7 +379,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
       register_with_sort InProp;
       register_with_sort InSet
   in
-  let ((id,(entry,g_kind)),hook) =
+  let id,entry,hook =
     build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
     proof_tac hook
   in
@@ -388,7 +387,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
      Don't forget to close the goal if an error is raised !!!!
   *)
   let uctx = Evd.evar_universe_context sigma in
-  save new_princ_name entry ~hook uctx g_kind
+  save new_princ_name entry ~hook uctx Decl_kinds.(Global ImportDefaultBehavior) Decl_kinds.(Proof Theorem)
   with e when CErrors.noncritical e ->
     raise (Defining_principle e)
 
@@ -519,7 +518,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Pro
         s::l_schemes -> s,l_schemes
       | _ -> anomaly (Pp.str "")
   in
-  let ((_,(const,_)),_) =
+  let _,const,_ =
     try
       build_functional_principle evd false
         first_type
@@ -577,10 +576,10 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Pro
 
              )
              ta;
-           (* If we reach this point, the two principle are not mutually recursive
-              We fall back to the previous method
-           *)
-             let ((_,(const,_)),_) =
+             (* If we reach this point, the two principle are not mutually recursive
+                We fall back to the previous method
+                *)
+             let _,const,_ =
                build_functional_principle
                  evd
                  false
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 0ecfbacb09..b07a92658b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -416,8 +416,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
       let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
       ComDefinition.do_definition
         ~program_mode:false
-        fname
-        Decl_kinds.(Global ImportDefaultBehavior,false,Definition) pl
+        ~name:fname
+        ~poly:false
+        ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+        ~kind:Decl_kinds.Definition pl
         bl None body (Some ret_type);
        let evd,rev_pconstants =
          List.fold_left
@@ -434,7 +436,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        None, evd,List.rev rev_pconstants
     | _ ->
-       ComFixpoint.do_fixpoint (Global ImportDefaultBehavior) false fixpoint_exprl;
+       ComFixpoint.do_fixpoint ~scope:(Global ImportDefaultBehavior) ~poly:false fixpoint_exprl;
        let evd,rev_pconstants =
          List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a5a07934ac..8745853180 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -123,7 +123,7 @@ open Declare
 
 let definition_message = Declare.definition_message
 
-let save id const ?hook uctx (locality,kind) =
+let save id const ?hook uctx locality kind =
   let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
   let r = match locality with
     | Discharge ->
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 1d096fa488..602f7af57a 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -47,7 +47,8 @@ val save
   -> Evd.side_effects Proof_global.proof_entry
   -> ?hook:DeclareDef.Hook.t
   -> UState.t
-  -> Decl_kinds.goal_kind
+  -> Decl_kinds.locality
+  -> Decl_kinds.goal_object_kind
   -> unit
 
 (* [with_full_print f a] applies [f] to [a] in full printing environment.
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index e5b0a5d032..1ab64ac1b2 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -803,10 +803,13 @@ 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 info = Lemmas.Info.make
+             ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+             ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
          let lemma = Lemmas.start_lemma
              ~name:lem_id
              ~poly:false
-             ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem)
+             ~info
              !evd
              typ in
          let lemma = fst @@ Lemmas.by
@@ -866,13 +869,14 @@ 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 lemma = Lemmas.start_lemma ~name:lem_id
-             ~poly:false
-             ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem) sigma
-             (fst lemmas_types_infos.(i)) in
+         let info = Lemmas.Info.make
+             ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+             ~kind:Decl_kinds.(Proof Theorem) () in
+         let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info
+             sigma (fst lemmas_types_infos.(i)) in
          let lemma = fst (Lemmas.by
-           (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
-              (proving_tac i))) lemma) in
+                            (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
+                                                     (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
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 187d907dc5..6663fa5c60 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1367,11 +1367,12 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
     in
     Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None
   in
-  let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in
+  let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook)
+      ~scope:Decl_kinds.(Global ImportDefaultBehavior) ~kind:Decl_kinds.(Proof Lemma)
+      () in
   let lemma = Lemmas.start_lemma
       ~name:na
-      ~poly:false (* FIXME *)
-      ~kind:Decl_kinds.(Global ImportDefaultBehavior, Proof Lemma) ~info
+      ~poly:false (* FIXME *) ~info
       sigma gls_type in
   let lemma = if Indfun_common.is_strict_tcc  ()
   then
@@ -1410,10 +1411,9 @@ let com_terminate
     nb_args ctx
     hook =
   let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
-    let info = Lemmas.Info.make ~hook () in
+    let info = Lemmas.Info.make ~hook ~scope:(Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in
     let lemma = Lemmas.start_lemma ~name:thm_name
         ~poly:false (*FIXME*)
-        ~kind:(Global ImportDefaultBehavior, Proof Lemma)
         ~sign:(Environ.named_context_val env)
         ~info
         ctx
@@ -1462,7 +1462,7 @@ 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 lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~kind:(Global ImportDefaultBehavior, Proof Lemma) ~sign evd
+    let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~sign evd
        (EConstr.of_constr equation_lemma_type) in
     let lemma = fst @@ Lemmas.by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index d87b7a1770..8d95c22529 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1995,9 +1995,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
   let poly = atts.polymorphic in
-  let kind = Decl_kinds.(Global ImportDefaultBehavior),
-             Decl_kinds.DefinitionBody Decl_kinds.Instance
-  in
+  let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
   let hook _ _ _ = function
     | Globnames.ConstRef cst ->
@@ -2008,10 +2006,10 @@ let add_morphism_interactive atts m n : Lemmas.t =
     | _ -> assert false
   in
   let hook = DeclareDef.Hook.make hook in
-  let info = Lemmas.Info.make ~hook () in
+  let info = Lemmas.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->
-       let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~kind ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+       let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
        fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
-- 
cgit v1.2.3


From b2aae7ba35a90e695d34f904c74f5156385344a9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Jun 2019 13:21:48 +0200
Subject: [api] Move `locality` from `library` to `vernac`.

This datatype does belong to this layer.
---
 plugins/funind/functional_principles_proofs.ml | 2 +-
 plugins/funind/functional_principles_types.ml  | 2 +-
 plugins/funind/indfun.ml                       | 4 ++--
 plugins/funind/indfun_common.ml                | 2 +-
 plugins/funind/indfun_common.mli               | 2 +-
 plugins/funind/invfun.ml                       | 4 ++--
 plugins/funind/recdef.ml                       | 4 ++--
 7 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0d3c7b365f..a904b81d81 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -991,7 +991,7 @@ 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 info = Lemmas.Info.make
-      ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
       ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
 
   let lemma = Lemmas.start_lemma
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 65b114fc03..1f8bf5be22 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -387,7 +387,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
      Don't forget to close the goal if an error is raised !!!!
   *)
   let uctx = Evd.evar_universe_context sigma in
-  save new_princ_name entry ~hook uctx Decl_kinds.(Global ImportDefaultBehavior) Decl_kinds.(Proof Theorem)
+  save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decl_kinds.(Proof Theorem)
   with e when CErrors.noncritical e ->
     raise (Defining_principle e)
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index b07a92658b..d305a58ccc 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -418,7 +418,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
         ~program_mode:false
         ~name:fname
         ~poly:false
-        ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+        ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
         ~kind:Decl_kinds.Definition pl
         bl None body (Some ret_type);
        let evd,rev_pconstants =
@@ -436,7 +436,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        None, evd,List.rev rev_pconstants
     | _ ->
-       ComFixpoint.do_fixpoint ~scope:(Global ImportDefaultBehavior) ~poly:false fixpoint_exprl;
+       ComFixpoint.do_fixpoint ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl;
        let evd,rev_pconstants =
          List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 8745853180..254760cb50 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -118,8 +118,8 @@ let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl"))
 (* Copy of the standard save mechanism but without the much too  *)
 (* slow reduction function                                       *)
 (*****************************************************************)
-open Decl_kinds
 open Declare
+open DeclareDef
 
 let definition_message = Declare.definition_message
 
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 602f7af57a..45d332031f 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -47,7 +47,7 @@ val save
   -> Evd.side_effects Proof_global.proof_entry
   -> ?hook:DeclareDef.Hook.t
   -> UState.t
-  -> Decl_kinds.locality
+  -> DeclareDef.locality
   -> Decl_kinds.goal_object_kind
   -> unit
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 1ab64ac1b2..587e1fc2e8 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -804,7 +804,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let lem_id = mk_correct_id f_id in
          let (typ,_) = lemmas_types_infos.(i) in
          let info = Lemmas.Info.make
-             ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+             ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
              ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
          let lemma = Lemmas.start_lemma
              ~name:lem_id
@@ -870,7 +870,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
            i*)
          let lem_id = mk_complete_id f_id in
          let info = Lemmas.Info.make
-             ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+             ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
              ~kind:Decl_kinds.(Proof Theorem) () in
          let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info
              sigma (fst lemmas_types_infos.(i)) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 6663fa5c60..425e498330 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1368,7 +1368,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
     Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None
   in
   let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook)
-      ~scope:Decl_kinds.(Global ImportDefaultBehavior) ~kind:Decl_kinds.(Proof Lemma)
+      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decl_kinds.Proof Decl_kinds.Lemma)
       () in
   let lemma = Lemmas.start_lemma
       ~name:na
@@ -1411,7 +1411,7 @@ let com_terminate
     nb_args ctx
     hook =
   let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
-    let info = Lemmas.Info.make ~hook ~scope:(Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in
+    let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in
     let lemma = Lemmas.start_lemma ~name:thm_name
         ~poly:false (*FIXME*)
         ~sign:(Environ.named_context_val env)
-- 
cgit v1.2.3


From 9d65c49f05f946557df4c67b6e752f978e1e9352 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Jun 2019 15:10:50 +0200
Subject: [api] Remove `polymorphic` type alias, use labels instead.

This is more in-line with attributes and the rest of the API, and
makes some code significantly clearer (as in `foo true false false`,
etc...)
---
 plugins/funind/glob_term_to_relation.ml | 2 +-
 plugins/ltac/extratactics.mlg           | 2 +-
 plugins/ltac/rewrite.ml                 | 4 ++--
 plugins/setoid_ring/newring.ml          | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 201d953692..bb4e745fe9 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1506,7 +1506,7 @@ let do_build_inductive
   let _time2 = System.get_time () in
   try
     with_full_print
-      (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false false false ~uniform:ComInductive.NonUniformParameters))
+      (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false ~poly:false false ~uniform:ComInductive.NonUniformParameters))
       Declarations.Finite
   with
     | UserError(s,msg) as e ->
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 49d8ab4e23..1e2b23bf96 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -328,7 +328,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
         if poly then ctx
 	else (* This is a global universe context that shouldn't be
 	        refreshed at every use of the hint, declare it globally. *)
-	  (Declare.declare_universe_context false ctx;
+          (Declare.declare_universe_context ~poly:false ctx;
            Univ.ContextSet.empty)
     in
       CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 8d95c22529..9d928232c6 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1795,7 +1795,7 @@ let declare_an_instance n s args =
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance atts binders (name,t) fields =
-  let _id = Classes.new_instance atts.polymorphic
+  let _id = Classes.new_instance ~poly:atts.polymorphic
       name binders t (true, CAst.make @@ CRecord (fields))
       ~global:atts.global ~generalize:false Hints.empty_hint_info
   in
@@ -2023,7 +2023,7 @@ let add_morphism atts binders m s n =
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
   let _id, lemma = Classes.new_instance_interactive
-      ~global:atts.global atts.polymorphic
+      ~global:atts.global ~poly:atts.polymorphic
       instance_name binders instance_t
       ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
   in
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 9bbe339770..33798c43c8 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -153,7 +153,7 @@ let decl_constant na univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
   let univs = UState.restrict_universe_context univs vars in
-  let () = Declare.declare_universe_context false univs in
+  let () = Declare.declare_universe_context ~poly:false univs in
   let types = (Typeops.infer (Global.env ()) c).uj_type in
   let univs = Monomorphic_entry Univ.ContextSet.empty in
   mkConst(declare_constant (Id.of_string na) 
-- 
cgit v1.2.3


From da5bbda84bd22b87a6057175c9d4d2391808e294 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Jun 2019 17:28:26 +0200
Subject: [api] [proof] Move `discharge` type to vernac_ast where it is used.

This seems like the right location, a bit more refactoring should be
possible.
---
 plugins/funind/g_indfun.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index ef9d91c7fa..e20d010c71 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -182,7 +182,7 @@ let is_proof_termination_interactively_checked recsl =
 
 let classify_as_Fixpoint recsl =
  Vernac_classifier.classify_vernac
-    (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
+    (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(NoDischarge, List.map snd recsl))))
 
 let classify_funind recsl =
   match classify_as_Fixpoint recsl with
-- 
cgit v1.2.3


From 0c47ebf825690675cbb71153b8c9e4f7f6858984 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 11 Jun 2019 02:02:15 +0200
Subject: [proof] API Documentation fixes.

---
 plugins/funind/functional_principles_types.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1f8bf5be22..edda2f2eef 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -324,10 +324,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   (*    end; *)
 
   let open Proof_global in
-  let { id; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+  let { name; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
   match entries with
   | [entry] ->
-    id, entry, hook
+    name, entry, hook
   | _ ->
     CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
 
-- 
cgit v1.2.3