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

5 files changed, 11 insertions, 9 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 76d427add..3c133f317 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -293,7 +293,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
       (* Check that the type is free of evars now. *)
       Pretyping.check_evars env Evd.empty sigma termtype;
       let termtype = to_constr sigma termtype in
-      let term = Option.map (to_constr sigma) term in
+      let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
         if not (Evd.has_undefined sigma) && not (Option.is_empty term) then
 	  declare_instance_constant k pri global imps ?hook id decl
             poly sigma (Option.get term) termtype
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index b18a60a1f..9aa61ab46 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -88,8 +88,8 @@ let interp_definition pl bl poly red_option c ctypopt =
   let evd = Evd.minimize_universes evd in
   (* Substitute evars and universes, and add parameters.
      Note: in program mode some evars may remain. *)
-  let ctx = List.map (EConstr.to_rel_decl evd) ctx in
-  let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr evd c) ctx in
+  let ctx = List.map Termops.(map_rel_decl (to_constr ~abort_on_undefined_evars:false evd)) ctx in
+  let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd c) ctx in
   let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr evd ty) ctx) tyopt in
   (* Keep only useful universes. *)
   let uvars_fold uvars c =
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index a794c2db0..1466fa243 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -225,7 +225,8 @@ let interp_recursive ~program_mode ~cofix fixl notations =
   (* Instantiate evars and check all are resolved *)
   let sigma = solve_unif_constraints_with_heuristics env_rec sigma in
   let sigma, _ = nf_evars_and_universes sigma in
-  let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr sigma) c) fixdefs in
+  (* XXX: We still have evars here in Program *)
+  let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr ~abort_on_undefined_evars:false sigma) c) fixdefs in
   let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in
   let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
 
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index b95741ca4..745f1df1d 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -229,7 +229,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   in
   (* XXX: Capturing sigma here... bad bad *)
   let hook = Lemmas.mk_hook (hook sigma) in
-  let fullcoqc = EConstr.to_constr sigma def in
+  (* XXX: Grounding non-ground terms here... bad bad *)
+  let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
   let fullctyp = EConstr.to_constr sigma typ in
   Obligations.check_evars env sigma;
   let evars, _, evars_def, evars_typ =
@@ -261,9 +262,10 @@ let do_program_recursive local poly fixkind fixl ntns =
   let collect_evars id def typ imps =
     (* Generalize by the recursive prototypes  *)
     let def =
-      EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)
+      EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)
     and typ =
-      EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)
+      (* Worrying... *)
+      EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)
     in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ =
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 698ee4703..23c863cab 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -640,8 +640,7 @@ let explain_refiner_cannot_generalize env sigma ty =
   pr_leconstr_env env sigma ty ++ str "."
 
 let explain_no_occurrence_found env sigma c id =
-  let c = EConstr.to_constr sigma c in
-  str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++
+  str "Found no subterm matching " ++ pr_leconstr_env env sigma c ++
   str " in " ++
     (match id with
       | Some id -> Id.print id