[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/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 285991797..83fbc2d5d 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -77,14 +77,14 @@ module CM=Map.Make(Constr)
 module History=Set.Make(Hitem)
 
 let cm_add sigma typ nam cm=
-  let typ = EConstr.to_constr sigma typ in
+  let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
   try
     let l=CM.find typ cm in CM.add typ (nam::l) cm
   with
       Not_found->CM.add typ [nam] cm
 
 let cm_remove sigma typ nam cm=
-  let typ = EConstr.to_constr sigma typ in
+  let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
   try
     let l=CM.find typ cm in
     let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in
@@ -152,7 +152,7 @@ let re_add_formula_list sigma lf seq=
      redexes=List.fold_right HP.add lf seq.redexes;
      context=List.fold_right do_one lf seq.context}
 
-let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr sigma t) seq.context)
+let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) seq.context)
 
 (*let rev_left seq=
   try