aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-02-27 15:33:11 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-02-27 15:33:11 +0100
commit52d90aee0859e5b67102435c6aee5c097c7ce4ce (patch)
tree3943603bfd0d7ab98206cdbd2b59372fe35876e3
parente3124e098ef8170dac2b348b91757a7034bc4999 (diff)
Add a comment on EConstr.to_constr regarding evar-freeness.
-rw-r--r--engine/eConstr.mli5
1 files changed, 4 insertions, 1 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 6fa338c73..01847fe07 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