Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contains evars

1 files changed, 2 insertions, 2 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4962b89a09..2c371d5cfa 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -117,7 +117,7 @@ open ExtraEnv
 exception Found of int array
 
 let nf_fix sigma (nas, cs, ts) =
-  let inj c = EConstr.to_constr sigma c in
+  let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
   (nas, Array.map inj cs, Array.map inj ts)
 
 let search_guard ?loc env possible_indexes fixdefs =
@@ -1150,7 +1150,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D
            (* Correction of bug #5315 : we need to define an evar for *all* holes *)
            let evkt = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s) in
            let ev,_ = destEvar !evdref evkt in
-           evdref := Evd.define ev (to_constr !evdref v) !evdref;
+           evdref := Evd.define ev (to_constr ~abort_on_undefined_evars:false !evdref v) !evdref;
            (* End of correction of bug #5315 *)
            { utj_val = v;
 	     utj_type = s }