diff options
| author | Matthieu Sozeau | 2018-08-15 20:14:57 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 11:17:56 +0100 |
| commit | 8a5cd826ee8d7d51c85c834c28f090466dda33a5 (patch) | |
| tree | 52aa7e5a2321ddac14847ef9f28e666664b4c11b /pretyping/evarconv.mli | |
| parent | acc4f5922dcc1f92f3dc3db653b7608949b60c2b (diff) | |
[occur_rigidly] Try improving occur-check approximation
The code is cleaner and more self-explanatory this way.
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 430dff2091..fa6f3466f6 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -120,6 +120,9 @@ val evar_eqappr_x : ?rhs_is_already_stuck:bool -> unify_flags -> env -> evar_map -> conv_pb -> state * Cst_stack.t -> state * Cst_stack.t -> Evarsolve.unification_result + +val occur_rigidly : Evarsolve.unify_flags -> + 'a -> Evd.evar_map -> Evar.t * 'b -> EConstr.t -> bool (**/**) (** {6 Functions to deal with impossible cases } *) |