diff options
| author | Maxime Dénès | 2018-02-28 10:16:15 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-28 10:16:15 +0100 |
| commit | 739e27be625a03db2d9d6651542eac7ccff8f4c2 (patch) | |
| tree | 4f3aae3685247c6c6536bd0192e5b959a6897b64 | |
| parent | e8c2d7a2f269eaa0c3b75d75680893f6af5dd29e (diff) | |
| parent | 52d90aee0859e5b67102435c6aee5c097c7ce4ce (diff) | |
Merge PR #6853: Add a comment on EConstr.to_constr regarding evar-freeness.
| -rw-r--r-- | engine/eConstr.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 6fa338c73d..01847fe078 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -67,7 +67,10 @@ val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_ter val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t, Sorts.t, Univ.Instance.t) Constr.kind_of_term val to_constr : Evd.evar_map -> t -> Constr.t -(** Returns the evar-normal form of the argument. See {!Evarutil.nf_evar}. *) +(** Returns the evar-normal form of the argument, and cast it as a theoretically + evar-free term. In practice this function does not check that the result + is actually evar-free, it is currently the duty of the caller to do so. + This might change in the future. *) val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type |