diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-04 15:54:28 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-31 18:44:19 +0200 |
| commit | 9f723f14e5342c1303646b5ea7bb5c0012a090ef (patch) | |
| tree | d6a6a82ab8b73e975588a547eb15a5a2f83fd4c7 /engine/eConstr.mli | |
| parent | 2d2d16430822f1768ce4f3c62ef0750b94e4747f (diff) | |
[econstr] Forbid calling `to_constr` in open terms.
We forbid calling `EConstr.to_constr` on terms that are not evar-free,
as to progress towards enforcing the invariant that `Constr.t` is
evar-free. [c.f. #6308]
Due to compatibility constraints we provide an optional parameter to
`to_constr`, `abort` which can be used to overcome this restriction
until we fix all parts of the code.
Now, grepping for `~abort:false` should return the questionable
parts of the system.
Not a lot of places had to be fixed, some comments:
- problems with the interface due to `Evd/Constr` [`Evd.define` being
the prime example] do seem real!
- inductives also look bad with regards to `Constr/EConstr`.
- code in plugins needs work.
A notable user of this "feature" is `Obligations/Program` that seem to
like to generate kernel-level entries with free evars, then to scan
them and workaround this problem by generating constants.
Diffstat (limited to 'engine/eConstr.mli')
| -rw-r--r-- | engine/eConstr.mli | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 28c9dd3c2..dac937457 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -68,11 +68,14 @@ 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, 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 to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t +(** Returns the evar-normal form of the argument. Note that this + function is supposed to be called when the original term has not + more free-evars anymore. If you need compatibility with the old + semantics, set [abort_on_undefined_evars] to [false]. + + For getting the evar-normal form of a term with evars see + {!Evarutil.nf_evar}. *) val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type |