diff options
| author | Pierre-Marie Pédrot | 2015-11-17 12:39:35 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-17 14:25:12 +0100 |
| commit | af399d81b0505d1f0be8e73cf45044266d5749e5 (patch) | |
| tree | 1723eebf74e332635ad08a1d5dc073363f051bcd /proofs/clenv.mli | |
| parent | 8e482fc932fa2b1893025d914d42dd17881c2fac (diff) | |
Performance fix for destruct.
The clenv_fchain function was needlessly merging universes coming from
two evarmaps even though one was an extension of the other. A flag was
added so that the tactic just retrieves the newer universes.
Diffstat (limited to 'proofs/clenv.mli')
| -rw-r--r-- | proofs/clenv.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index eb10817069..26e803354e 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -51,7 +51,7 @@ val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst val connect_clenv : Goal.goal sigma -> clausenv -> clausenv val clenv_fchain : - ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv + ?with_univs:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv (** {6 Unification with clenvs } *) |