[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.

1 files changed, 3 insertions, 3 deletions

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 4c834f2f8..c4eb6af89 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -35,7 +35,7 @@ let meta_type evd mv =
 let inductive_type_knowing_parameters env sigma (ind,u) jl =
   let u = Unsafe.to_instance u in
   let mspec = lookup_mind_specif env ind in
-  let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
+  let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in
   Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
 
 let e_type_judgment env evdref j =
@@ -155,7 +155,7 @@ let e_type_case_branches env evdref (ind,largs) pj c =
   let p = pj.uj_val in
   let params = List.map EConstr.Unsafe.to_constr params in
   let () = e_is_correct_arity env evdref c pj ind specif params in
-  let lc = build_branches_type ind specif params (EConstr.to_constr !evdref p) in
+  let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false !evdref p) in
   let lc = Array.map EConstr.of_constr lc in
   let n = (snd specif).Declarations.mind_nrealdecls in
   let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in
@@ -207,7 +207,7 @@ let enrich_env env evdref =
   Environ.env_of_pre_env penv'
 
 let check_fix env sigma pfix =
-  let inj c = EConstr.to_constr sigma c in
+  let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
   let (idx, (ids, cs, ts)) = pfix in
   check_fix env (idx, (ids, Array.map inj cs, Array.map inj ts))