diff options
| -rw-r--r-- | ide/utils/uoptions.mli | 148 | ||||
| -rw-r--r-- | parsing/g_minicoq.mli | 31 | ||||
| -rw-r--r-- | toplevel/fhimsg.mli | 74 | ||||
| -rw-r--r-- | toplevel/searchisos.mli | 16 |
4 files changed, 0 insertions, 269 deletions
diff --git a/ide/utils/uoptions.mli b/ide/utils/uoptions.mli deleted file mode 100644 index a323ac605..000000000 --- a/ide/utils/uoptions.mli +++ /dev/null @@ -1,148 +0,0 @@ -(**************************************************************************) -(* Cameleon *) -(* *) -(* Copyright (C) 2002 Institut National de Recherche en Informatique et *) -(* en Automatique. All rights reserved. *) -(* *) -(* This program is free software; you can redistribute it and/or modify *) -(* it under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation; either version 2 of the License, or *) -(* any later version. *) -(* *) -(* This program is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) -(* GNU General Public License for more details. *) -(* *) -(* You should have received a copy of the GNU General Public License *) -(* along with this program; if not, write to the Free Software *) -(* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA *) -(* 02111-1307 USA *) -(* *) -(* Contact: Maxence.Guesdon@inria.fr *) -(**************************************************************************) - -(** - This module implements a simple mechanism to handle program options files. - An options file is defined as a set of [variable = value] lines, - where value can be a simple string, a list of values (between brackets -or parentheses) or a set of [variable = value] lines between braces. -The option file is automatically loaded and saved, and options are -manipulated inside the program as easily as references. - - Code from Fabrice Le Fessant. -*) - -type 'a option_class -(** The abstract type for a class of options. A class is a set of options -which use the same conversion functions from loading and saving.*) - -type 'a option_record -(** The abstract type for an option *) - -type options_file - -val create_options_file : string -> options_file -val set_options_file : options_file -> string -> unit -val prune_file : options_file -> unit - -(** {2 Operations on option files} *) - -val load : options_file -> unit -(** [load file] loads the option file. All options whose value is specified - in the option file are updated. *) - -val append : options_file -> string -> unit -(** [append filename] loads the specified option file. All options whose -value is specified in this file are updated. *) - -val save : options_file -> unit -(** [save file] saves all the options values to the option file. *) - -val save_with_help : options_file -> unit -(** [save_with_help ()] saves all the options values to the option file, - with the help provided for each option. *) - -(** {2 Creating options} *) - -val define_option : options_file -> - string list -> string -> 'a option_class -> 'a -> 'a option_record -val option_hook : 'a option_record -> (unit -> unit) -> unit - -val string_option : string option_class -val color_option : string option_class -val font_option : string option_class -val int_option : int option_class -val bool_option : bool option_class -val float_option : float option_class -val string2_option : (string * string) option_class - - (* parameterized options *) -val list_option : 'a option_class -> 'a list option_class -val smalllist_option : 'a option_class -> 'a list option_class -val sum_option : (string * 'a) list -> 'a option_class -val tuple2_option : - 'a option_class * 'b option_class -> ('a * 'b) option_class -val tuple3_option : 'a option_class * 'b option_class * 'c option_class -> - ('a * 'b * 'c) option_class -val tuple4_option : - 'a option_class * 'b option_class * 'c option_class * 'd option_class -> - ('a * 'b * 'c * 'd) option_class - -(** {2 Using options} *) - -val ( !! ) : 'a option_record -> 'a -val ( =:= ) : 'a option_record -> 'a -> unit - -val shortname : 'a option_record -> string -val get_help : 'a option_record -> string - -(** {2 Creating new option classes} *) - -val get_class : 'a option_record -> 'a option_class - -val class_hook : 'a option_class -> ('a option_record -> unit) -> unit - -type option_value = - Module of option_module -| StringValue of string -| IntValue of int -| FloatValue of float -| List of option_value list -| SmallList of option_value list - -and option_module = - (string * option_value) list - -val define_option_class : - string -> (option_value -> 'a) -> ('a -> option_value) -> 'a option_class - -val to_value : 'a option_class -> 'a -> option_value -val from_value : 'a option_class -> option_value -> 'a - -val value_to_string : option_value -> string -val string_to_value : string -> option_value -val value_to_int : option_value -> int -val int_to_value : int -> option_value -val bool_of_string : string -> bool -val value_to_bool : option_value -> bool -val bool_to_value : bool -> option_value -val value_to_float : option_value -> float -val float_to_value : float -> option_value -val value_to_string2 : option_value -> string * string -val string2_to_value : string * string -> option_value -val value_to_list : (option_value -> 'a) -> option_value -> 'a list -val list_to_value : ('a -> option_value) -> 'a list -> option_value -val smalllist_to_value : ('a -> option_value) -> 'a list -> option_value - -val set_simple_option : options_file -> string -> string -> unit -val simple_options : options_file -> (string * string) list -val get_simple_option : options_file -> string -> string -val set_option_hook : options_file -> string -> (unit -> unit) -> unit - -val set_string_wrappers : 'a option_record -> - ('a -> string) -> (string -> 'a) -> unit - -(** {2 Other functions} *) - -val simple_args : options_file -> (string * Arg.spec * string) list diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli deleted file mode 100644 index 5b4db848e..000000000 --- a/parsing/g_minicoq.mli +++ /dev/null @@ -1,31 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ i*) - -(*i*) -open Pp -open Names -open Term -open Environ -(*i*) - -val term : constr Grammar.Entry.e - -type command = - | Definition of identifier * constr option * constr - | Parameter of identifier * constr - | Variable of identifier * constr - | Inductive of - (identifier * constr) list * - (identifier * constr * (identifier * constr) list) list - | Check of constr - -val command : command Grammar.Entry.e - -val pr_term : path_kind -> env -> constr -> std_ppcmds diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli deleted file mode 100644 index d29e38057..000000000 --- a/toplevel/fhimsg.mli +++ /dev/null @@ -1,74 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ i*) - -(*i*) -open Pp -open Names -open Term -open Sign -open Environ -open Type_errors -(*i*) - -(* This module provides functions to explain the various typing errors. - It is parameterized by a function to pretty-print a term in a given - context. *) - -module type Printer = sig - val pr_term : path_kind -> env -> constr -> std_ppcmds -end - -(*s The result is a module which provides a function [explain_type_error] - to explain a type error for a given kind in a given env, which are - usually the three arguments carried by the exception [TypeError] - (see \refsec{typeerrors}). *) - -module Make (P : Printer) : sig - -val explain_type_error : path_kind -> env -> type_error -> std_ppcmds - -val pr_ne_ctx : std_ppcmds -> path_kind -> env -> std_ppcmds - -val explain_unbound_rel : path_kind -> env -> int -> std_ppcmds - -val explain_not_type : path_kind -> env -> constr -> std_ppcmds - -val explain_bad_assumption : path_kind -> env -> constr -> std_ppcmds - -val explain_reference_variables : identifier -> std_ppcmds - -val explain_elim_arity : - path_kind -> env -> constr -> constr list -> constr - -> unsafe_judgment -> (constr * constr * string) option -> std_ppcmds - -val explain_case_not_inductive : - path_kind -> env -> unsafe_judgment -> std_ppcmds - -val explain_number_branches : - path_kind -> env -> unsafe_judgment -> int -> std_ppcmds - -val explain_ill_formed_branch : - path_kind -> env -> constr -> int -> constr -> constr -> std_ppcmds - -val explain_generalization : - path_kind -> env -> name * types -> constr -> std_ppcmds - -val explain_actual_type : - path_kind -> env -> constr -> constr -> constr -> std_ppcmds - -val explain_ill_formed_rec_body : - path_kind -> env -> guard_error -> - name array -> int -> constr array -> std_ppcmds - -val explain_ill_typed_rec_body : - path_kind -> env -> int -> name list -> unsafe_judgment array - -> types array -> std_ppcmds - -end diff --git a/toplevel/searchisos.mli b/toplevel/searchisos.mli deleted file mode 100644 index b9ad28ad0..000000000 --- a/toplevel/searchisos.mli +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ i*) - -val search_in_lib : bool ref -val type_search : Term.constr -> unit -val require_module2 : bool option -> string -> string option -> bool -> unit -val upd_tbl_ind_one : unit -> unit -val seetime : bool ref -val load_leaf_entry : string -> Names.section_path * Libobject.obj -> unit |