diff options
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 104 |
1 files changed, 47 insertions, 57 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index cf47d194e3..34bafdb23c 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -23,7 +23,7 @@ open Evarutil (** An auxiliary function for searching for fixpoint guard indexes *) val search_guard : - Pp.loc -> env -> int list list -> rec_declaration -> int array + Pp.loc -> env -> int list list -> rec_declaration -> int array type typing_constraint = OfType of types option | IsType @@ -33,82 +33,72 @@ type ltac_var_map = var_map * unbound_ltac_var_map type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr -module type S = -sig +(** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) +val allow_anonymous_refs : bool ref + +(** Generic call to the interpreter from glob_constr to open_constr, leaving + unresolved holes as evars and returning the typing contexts of + these evars. Work as [understand_gen] for the rest. *) - module Cases : Cases.S +val understand_tcc : ?resolve_classes:bool -> + evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr - (** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) - val allow_anonymous_refs : bool ref +val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool -> + evar_map ref -> env -> typing_constraint -> glob_constr -> constr - (** Generic call to the interpreter from glob_constr to open_constr, leaving - unresolved holes as evars and returning the typing contexts of - these evars. Work as [understand_gen] for the rest. *) +(** More general entry point with evars from ltac *) - val understand_tcc : ?resolve_classes:bool -> - evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr +(** Generic call to the interpreter from glob_constr to constr, failing + unresolved holes in the glob_constr cannot be instantiated. - val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool -> - evar_map ref -> env -> typing_constraint -> glob_constr -> constr + In [understand_ltac expand_evars sigma env ltac_env constraint c], - (** More general entry point with evars from ltac *) + expand_evars : expand inferred evars by their value if any + sigma : initial set of existential variables (typically dependent subgoals) + ltac_env : partial substitution of variables (used for the tactic language) + constraint : tell if interpreted as a possibly constrained term or a type +*) - (** Generic call to the interpreter from glob_constr to constr, failing - unresolved holes in the glob_constr cannot be instantiated. +val understand_ltac : + bool -> evar_map -> env -> ltac_var_map -> + typing_constraint -> glob_constr -> pure_open_constr - In [understand_ltac expand_evars sigma env ltac_env constraint c], +(** Standard call to get a constr from a glob_constr, resolving implicit args *) - expand_evars : expand inferred evars by their value if any - sigma : initial set of existential variables (typically dependent subgoals) - ltac_env : partial substitution of variables (used for the tactic language) - constraint : tell if interpreted as a possibly constrained term or a type - *) +val understand : evar_map -> env -> ?expected_type:Term.types -> + glob_constr -> constr - val understand_ltac : - bool -> evar_map -> env -> ltac_var_map -> - typing_constraint -> glob_constr -> pure_open_constr +(** Idem but the glob_constr is intended to be a type *) - (** Standard call to get a constr from a glob_constr, resolving implicit args *) +val understand_type : evar_map -> env -> glob_constr -> constr - val understand : evar_map -> env -> ?expected_type:Term.types -> - glob_constr -> constr +(** A generalization of the two previous case *) - (** Idem but the glob_constr is intended to be a type *) +val understand_gen : typing_constraint -> evar_map -> env -> + glob_constr -> constr - val understand_type : evar_map -> env -> glob_constr -> constr +(** Idem but returns the judgment of the understood term *) - (** A generalization of the two previous case *) +val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment - val understand_gen : typing_constraint -> evar_map -> env -> - glob_constr -> constr +(** Idem but do not fail on unresolved evars *) +val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment - (** Idem but returns the judgment of the understood term *) +(**/**) +(** Internal of Pretyping... *) +val pretype : + type_constraint -> env -> evar_map ref -> + ltac_var_map -> glob_constr -> unsafe_judgment - val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment +val pretype_type : + val_constraint -> env -> evar_map ref -> + ltac_var_map -> glob_constr -> unsafe_type_judgment - (** Idem but do not fail on unresolved evars *) - val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment +val pretype_gen : + bool -> bool -> bool -> evar_map ref -> env -> + ltac_var_map -> typing_constraint -> glob_constr -> constr - (**/**) - (** Internal of Pretyping... *) - val pretype : - type_constraint -> env -> evar_map ref -> - ltac_var_map -> glob_constr -> unsafe_judgment - - val pretype_type : - val_constraint -> env -> evar_map ref -> - ltac_var_map -> glob_constr -> unsafe_type_judgment - - val pretype_gen : - bool -> bool -> bool -> evar_map ref -> env -> - ltac_var_map -> typing_constraint -> glob_constr -> constr - - (**/**) - -end - -module Pretyping_F (C : Coercion.S) : S -module Default : S +(**/**) (** To embed constr in glob_constr *) |