diff options
Diffstat (limited to 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 61 |
1 files changed, 36 insertions, 25 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index c51cb0f4..32b94e1b 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -1,19 +1,26 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 *) +(* // * 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) *) (************************************************************************) open Names -open Term open Environ +open EConstr open Glob_term open Termops open Mod_subst open Misctypes open Evd +open Ltac_pretype + +type _ delay = +| Now : 'a delay +| Later : [ `thunk ] delay (** Should we keep details of universes during detyping ? *) val print_universes : bool ref @@ -21,39 +28,43 @@ val print_universes : bool ref (** If true, prints full local context of evars *) val print_evar_arguments : bool ref +(** If true, contract branches with same r.h.s. and same matching + variables in a disjunctive pattern *) +val print_factorize_match_patterns : bool ref + +(** If true and the last non unique clause of a "match" is a + variable-free disjunctive pattern, turn it into a catch-call case *) +val print_allow_match_default_clause : bool ref + val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern val subst_glob_constr : substitution -> glob_constr -> glob_constr +val factorize_eqns : 'a cases_clauses_g -> 'a disjunctive_cases_clauses_g + (** [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_names : bool -> Id.t list -> names_context -> env -> evar_map -> constr -> glob_constr - -val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob_constr +val detype_names : bool -> Id.Set.t -> names_context -> env -> evar_map -> constr -> glob_constr -val detype_case : - bool -> (constr -> glob_constr) -> - (constructor array -> bool list array -> constr array -> - (Loc.t * Id.t list * cases_pattern list * glob_constr) list) -> - (constr -> bool list -> bool) -> - Id.t list -> inductive * case_style * bool list array * bool list -> - constr option -> constr -> constr array -> glob_constr +val detype : 'a delay -> ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> constr -> 'a glob_constr_g -val detype_sort : evar_map -> sorts -> glob_sort +val detype_sort : evar_map -> Sorts.t -> glob_sort -val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> - evar_map -> Context.Rel.t -> glob_decl list +val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) -> + evar_map -> rel_context -> 'a glob_decl_g list -val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr +val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr (** look for the index of a named var or a nondep var as it is renamed *) -val lookup_name_as_displayed : env -> constr -> Id.t -> int option -val lookup_index_as_renamed : env -> constr -> int -> int option +val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option +val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option + +(* XXX: This is a hack and should go away *) +val set_detype_anonymous : (?loc:Loc.t -> int -> Id.t) -> unit -val set_detype_anonymous : (Loc.t -> int -> glob_constr) -> unit val force_wildcard : unit -> bool val synthetize_type : unit -> bool @@ -71,7 +82,7 @@ val subst_genarg_hook : module PrintingInductiveMake : functor (Test : sig val encode : Libnames.reference -> Names.inductive - val member_message : Pp.std_ppcmds -> bool -> Pp.std_ppcmds + val member_message : Pp.t -> bool -> Pp.t val field : string val title : string end) -> @@ -80,9 +91,9 @@ module PrintingInductiveMake : val compare : t -> t -> int val encode : Libnames.reference -> Names.inductive val subst : substitution -> t -> t - val printer : t -> Pp.std_ppcmds + val printer : t -> Pp.t val key : Goptions.option_name val title : string - val member_message : t -> bool -> Pp.std_ppcmds + val member_message : t -> bool -> Pp.t val synchronous : bool end |