diff options
| author | Matthieu Sozeau | 2014-05-02 11:34:53 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:59:01 +0200 |
| commit | 2de8910d2cc0af096e6d91b0ea165997ce144503 (patch) | |
| tree | 1e2345eea549fdc176f7abe17123a0be3051289b /pretyping/evarutil.mli | |
| parent | ce11f55e27c8e4f98384aacd61ee67c593340195 (diff) | |
- Fix treatment of global universe constraints which should be passed along
in the Evd of proofs (Evd.from_env).
- Allow to set the Store.t value of new evars, e.g. to set constraint evars as
unresolvable in rewrite.ml.
- Fix a HUGE performance problem in the processing of constraints, which was remerging
all the previous constraints with the ambient global universes at each new constraint addition.
Performance is now back to (or better than) normal.
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index d197ad2efe..7715691b0c 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -23,18 +23,18 @@ val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) val new_evar : evar_map -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> types -> evar_map * constr + ?candidates:constr list -> ?store:Store.t -> types -> evar_map * constr val new_pure_evar : evar_map -> named_context_val -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> types -> evar_map * evar + ?candidates:constr list -> ?store:Store.t -> types -> evar_map * evar val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar (** the same with side-effects *) val e_new_evar : evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> types -> constr + ?candidates:constr list -> ?store:Store.t -> types -> constr (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) @@ -57,7 +57,9 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context_val -> evar_map -> types -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> constr list -> evar_map * constr + named_context_val -> evar_map -> types -> + ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> + ?store:Store.t -> constr list -> evar_map * constr val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list |