summaryrefslogtreecommitdiff
path: root/pretyping/detyping.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/detyping.mli')
-rw-r--r--pretyping/detyping.mli60
1 files changed, 37 insertions, 23 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 556b2477..40e3d0f8 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -1,60 +1,74 @@
(************************************************************************)
(* 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-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: detyping.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Util
open Names
open Term
open Sign
open Environ
-open Rawterm
+open Glob_term
open Termops
open Mod_subst
-(*i*)
val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern
-val subst_rawconstr : substitution -> rawconstr -> rawconstr
+val subst_glob_constr : substitution -> glob_constr -> glob_constr
-(* [detype isgoal avoid ctx c] turns a closed [c], into a rawconstr *)
-(* de Bruijn indexes are turned to bound names, avoiding names in [avoid] *)
-(* [isgoal] tells if naming must avoid global-level synonyms as intro does *)
-(* [ctx] gives the names of the free variables *)
+(** [detype isgoal avoid ctx c] turns a closed [c], into a glob_constr
+ de Bruijn indexes are turned to bound names, avoiding names in [avoid]
+ [isgoal] tells if naming must avoid global-level synonyms as intro does
+ [ctx] gives the names of the free variables *)
-val detype : bool -> identifier list -> names_context -> constr -> rawconstr
+val detype : bool -> identifier list -> names_context -> constr -> glob_constr
val detype_case :
- bool -> ('a -> rawconstr) ->
+ bool -> ('a -> glob_constr) ->
(constructor array -> int array -> 'a array ->
- (loc * identifier list * cases_pattern list * rawconstr) list) ->
+ (loc * identifier list * cases_pattern list * glob_constr) list) ->
('a -> int -> bool) ->
identifier list -> inductive * case_style * int * int array * int ->
- 'a option -> 'a -> 'a array -> rawconstr
+ 'a option -> 'a -> 'a array -> glob_constr
-val detype_sort : sorts -> rawsort
+val detype_sort : sorts -> glob_sort
val detype_rel_context : constr option -> identifier list -> names_context ->
- rel_context -> rawdecl list
+ rel_context -> glob_decl list
-(* look for the index of a named var or a nondep var as it is renamed *)
+(** look for the index of a named var or a nondep var as it is renamed *)
val lookup_name_as_displayed : env -> constr -> identifier -> int option
val lookup_index_as_renamed : env -> constr -> int -> int option
-val set_detype_anonymous : (loc -> int -> rawconstr) -> unit
+val set_detype_anonymous : (loc -> int -> glob_constr) -> unit
val force_wildcard : unit -> bool
val synthetize_type : unit -> bool
-(* Utilities to transform kernel cases to simple pattern-matching problem *)
+(** Utilities to transform kernel cases to simple pattern-matching problem *)
-val it_destRLambda_or_LetIn_names : int -> rawconstr -> name list * rawconstr
+val it_destRLambda_or_LetIn_names : int -> glob_constr -> name list * glob_constr
val simple_cases_matrix_of_branches :
- inductive -> int list -> rawconstr list -> cases_clauses
+ inductive -> (int * int * glob_constr) list -> cases_clauses
val return_type_of_predicate :
- inductive -> int -> int -> rawconstr -> predicate_pattern * rawconstr option
+ inductive -> int -> int -> glob_constr -> predicate_pattern * glob_constr option
+
+module PrintingInductiveMake :
+ functor (Test : sig
+ val encode : Libnames.reference -> Names.inductive
+ val member_message : Pp.std_ppcmds -> bool -> Pp.std_ppcmds
+ val field : string
+ val title : string
+ end) ->
+ sig
+ type t = Names.inductive
+ val encode : Libnames.reference -> Names.inductive
+ val subst : substitution -> t -> t
+ val printer : t -> Pp.std_ppcmds
+ val key : Goptions.option_name
+ val title : string
+ val member_message : t -> bool -> Pp.std_ppcmds
+ val synchronous : bool
+ end