diff options
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index 44bf29266..c0479acf6 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -30,10 +30,7 @@ val build_mutual : (identifier * Coqast.t) list -> (identifier * Coqast.t * (identifier * Coqast.t) list) list -> bool -> unit -val build_mutual_give_path : - (identifier * Coqast.t) list -> - (identifier * Coqast.t * (identifier * Coqast.t) list) list -> bool - -> section_path +val declare_mutual_with_eliminations : Declarations.mutual_inductive_entry -> section_path val build_recursive : (identifier * ((identifier * Coqast.t) list) * Coqast.t * Coqast.t) list |