diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-10-21 18:16:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-10-21 18:16:16 +0200 |
| commit | 517cc63a18d95c02c2d2490adb110ff712d30375 (patch) | |
| tree | 22c6e527663803ceec47afc625bb1a2e5b75adad /engine/evarutil.mli | |
| parent | cef86ed6f78e2efa703bd8772a43fbeba597bbe3 (diff) | |
| parent | 5609da1e08f950fab85b87b257ed343b491f1ef5 (diff) | |
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Diffstat (limited to 'engine/evarutil.mli')
| -rw-r--r-- | engine/evarutil.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index c0c81442d..7fdc7aac7 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -110,6 +110,12 @@ val is_ground_env : evar_map -> env -> bool its (partial) definition. *) val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t +(** [advance sigma g] returns [Some g'] if [g'] is undefined and is + the current avatar of [g] (for instance [g] was changed by [clear] + into [g']). It returns [None] if [g] has been (partially) + solved. *) +val advance : evar_map -> evar -> evar option + (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. This is roughly a combination of the previous functions and |