diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-10 16:06:33 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 10:23:29 +0200 |
| commit | ce609ff2ae8bdf59d31919194a2e58d6feb43943 (patch) | |
| tree | 6a12557a042a49c6f127826e1b93aef9ae82c335 /pretyping/evarutil.mli | |
| parent | 2b12eb9574b7192d70605e9c707fc4b2f94b71d0 (diff) | |
Move the handling of the principal evar from refine to evd.
See previous commit for more discussion.
Changed the name from "main" to "principal" because I find "main" overused, and because the name was only introduced yesterday anyway.
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index f38c1ea0f..ea00f8067 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -24,12 +24,14 @@ val mk_new_meta : unit -> constr val new_evar : env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> types -> evar_map * constr + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> types -> evar_map * constr val new_pure_evar : named_context_val -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> types -> evar_map * evar + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> types -> evar_map * evar val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar @@ -37,18 +39,19 @@ val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar val e_new_evar : env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> types -> constr + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> types -> constr (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> rigid -> + ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> evar_map * (constr * sorts) val e_new_type_evar : env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> rigid -> constr * sorts + ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr @@ -71,6 +74,7 @@ val new_evar_instance : named_context_val -> evar_map -> types -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> constr list -> evar_map * constr val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list |