[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, 2 insertions, 2 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 96d80741a..0c109b026 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1592,14 +1592,14 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
       Id.Set.subset (collect_vars evd rhs) !names 
   in
   let body =
-    if fast rhs then EConstr.of_constr (EConstr.to_constr evd rhs) (** FIXME? *)
+    if fast rhs then nf_evar evd rhs (** FIXME? *)
     else
       let t' = imitate (env,0) rhs in
 	if !progress then
 	  (recheck_applications conv_algo (evar_env evi) evdref t'; t')
 	else t'
   in (!evdref,body)
-     
+
 (* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
  * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said,
  * [define] tries to find an instance lhs such that