diff options
| author | Pierre-Marie Pédrot | 2019-06-25 17:26:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-25 17:26:44 +0200 |
| commit | 7dfcb0f7c817e66280ab37b6c653b5596a16c249 (patch) | |
| tree | f59cbad4ef2e56070fe32fefcc5f7a3f8c6b7a4a /vernac/comFixpoint.mli | |
| parent | 7024688c4e20fa7b70ac1c550c166d02fce8d15c (diff) | |
| parent | c2abcaefd796b7f430f056884349b9d959525eec (diff) | |
Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec theorems.
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'vernac/comFixpoint.mli')
| -rw-r--r-- | vernac/comFixpoint.mli | 25 |
1 files changed, 4 insertions, 21 deletions
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index b42e877d41..982d316605 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -10,7 +10,6 @@ open Names open Constr -open Decl_kinds open Constrexpr open Vernacexpr @@ -19,16 +18,16 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint_interactive : - locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Lemmas.t + scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> Lemmas.t val do_fixpoint : - locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint_interactive : - locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t + scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t val do_cofixpoint : - locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit (************************************************************************) (** Internal API *) @@ -81,22 +80,6 @@ val interp_fixpoint : recursive_preentry * UState.universe_decl * UState.t * (EConstr.rel_context * Impargs.manual_implicits * int option) list -(** Registering fixpoints and cofixpoints in the environment *) - -(** [Not used so far] *) -val declare_fixpoint : - locality -> polymorphic -> - recursive_preentry * UState.universe_decl * UState.t * - (Constr.rel_context * Impargs.manual_implicits * int option) list -> - Lemmas.lemma_possible_guards -> decl_notation list -> - unit - -val declare_cofixpoint : - locality -> polymorphic -> - recursive_preentry * UState.universe_decl * UState.t * - (Constr.rel_context * Impargs.manual_implicits * int option) list -> - decl_notation list -> unit - (** Very private function, do not use *) val compute_possible_guardness_evidences : ('a, 'b) Context.Rel.pt * 'c * int option -> int list |