diff options
| author | Emilio Jesus Gallego Arias | 2019-05-23 05:59:20 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-24 20:53:42 +0200 |
| commit | aea3f5ab8befda178688f9b8bfb843e5081f4a08 (patch) | |
| tree | 853ce1c003d753bb8d581ab06c7fc1bf4621e74c /vernac/comFixpoint.mli | |
| parent | 4fa7abffb369925973e94cface4009db827c34de (diff) | |
[fixpoint] Remove code duplication in (co) fixpoint declaration.
Diffstat (limited to 'vernac/comFixpoint.mli')
| -rw-r--r-- | vernac/comFixpoint.mli | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index b42e877d41..8d76a30cee 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -81,22 +81,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 |