diff options
| author | Emilio Jesus Gallego Arias | 2019-07-17 07:11:41 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-31 11:13:04 +0200 |
| commit | 105269d6799356eb52f289e191217b153c3bdade (patch) | |
| tree | e62ad76ebf11c0af3f53263e2304844a2dff0fa1 /plugins/funind/indfun.mli | |
| parent | 7864ae92065ecb787c72cdd8eca2b3aeb6604dbe (diff) | |
[funind] Move principle generation to its own file.
Diffstat (limited to 'plugins/funind/indfun.mli')
| -rw-r--r-- | plugins/funind/indfun.mli | 23 |
1 files changed, 10 insertions, 13 deletions
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index bfc9686ae5..97a840e950 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,19 +1,16 @@ -open Names -open Tactypes - -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 : Vernacexpr.fixpoint_expr list -> unit - -val do_generate_principle_interactive : Vernacexpr.fixpoint_expr list -> Lemmas.t +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) val functional_induction : bool -> EConstr.constr -> - (EConstr.constr * EConstr.constr bindings) option -> + (EConstr.constr * EConstr.constr Tactypes.bindings) option -> Ltac_plugin.Tacexpr.or_and_intro_pattern option -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma - -val make_graph : GlobRef.t -> unit |