summaryrefslogtreecommitdiff
path: root/toplevel/indschemes.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/indschemes.mli')
-rw-r--r--toplevel/indschemes.mli26
1 files changed, 11 insertions, 15 deletions
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
index 707b9e00..8ce27708 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.mli
@@ -1,56 +1,52 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: indschemes.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Util
open Names
open Term
open Environ
open Libnames
-open Rawterm
+open Glob_term
open Genarg
open Vernacexpr
open Ind_tables
-(*i*)
-(* See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *)
+(** See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *)
-(* Build and register the boolean equalities associated to an inductive type *)
+(** Build and register the boolean equalities associated to an inductive type *)
val declare_beq_scheme : mutual_inductive -> unit
val declare_eq_decidability : mutual_inductive -> unit
-(* Build and register a congruence scheme for an equality-like inductive type *)
+(** Build and register a congruence scheme for an equality-like inductive type *)
val declare_congr_scheme : inductive -> unit
-(* Build and register rewriting schemes for an equality-like inductive type *)
+(** Build and register rewriting schemes for an equality-like inductive type *)
val declare_rewriting_schemes : inductive -> unit
-(* Mutual Minimality/Induction scheme *)
+(** Mutual Minimality/Induction scheme *)
val do_mutual_induction_scheme :
- (identifier located * bool * inductive * rawsort) list -> unit
+ (identifier located * bool * inductive * glob_sort) list -> unit
-(* Main calls to interpret the Scheme command *)
+(** Main calls to interpret the Scheme command *)
val do_scheme : (identifier located option * scheme) list -> unit
-(* Combine a list of schemes into a conjunction of them *)
+(** Combine a list of schemes into a conjunction of them *)
val build_combined_scheme : env -> constant list -> constr * types
val do_combined_scheme : identifier located -> identifier located list -> unit
-(* Hook called at each inductive type definition *)
+(** Hook called at each inductive type definition *)
val declare_default_schemes : mutual_inductive -> unit