From 43d381ab20035f64ce2edea8639fcd9e1d0453bc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 14:09:30 +0200
Subject: [declare] Move proof information to declare.

At this point the record in lemmas was just a stub; next commit will
stop exposing the internals of mutual information, and pave the way
for the refactoring of `Info.t` handling in the Declare interface.
---
 vernac/comFixpoint.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/comFixpoint.mli')

diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 62a9d10bae..486d0156f9 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -16,13 +16,13 @@ open Vernacexpr
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint_interactive :
-  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t
+  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t
 
 val do_fixpoint :
   scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit
 
 val do_cofixpoint_interactive :
-  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t
+  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t
 
 val do_cofixpoint :
   scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit
-- 
cgit v1.2.3


From a6d663c85d71b3cce007af23419e8030b8c5ac88 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 14:57:44 +0200
Subject: [declare] [api] Removal of duplicated type aliases.

---
 vernac/comFixpoint.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'vernac/comFixpoint.mli')

diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 486d0156f9..aa5446205c 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -16,16 +16,16 @@ open Vernacexpr
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint_interactive :
-  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t
+  scope:Locality.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t
 
 val do_fixpoint :
-  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit
+  scope:Locality.locality -> poly:bool -> fixpoint_expr list -> unit
 
 val do_cofixpoint_interactive :
-  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t
+  scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t
 
 val do_cofixpoint :
-  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit
+  scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> unit
 
 (************************************************************************)
 (** Internal API  *)
-- 
cgit v1.2.3