diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 418ea271c..1e53faccd 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1230,6 +1230,7 @@ let clos_norm_flags flgs env sigma t = let evars ev = safe_evar_value sigma ev in EConstr.of_constr (CClosure.norm_val (CClosure.create_clos_infos ~evars flgs env) + (CClosure.create_tab ()) (CClosure.inject (EConstr.Unsafe.to_constr t))) with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") @@ -1238,6 +1239,7 @@ let clos_whd_flags flgs env sigma t = let evars ev = safe_evar_value sigma ev in EConstr.of_constr (CClosure.whd_val (CClosure.create_clos_infos ~evars flgs env) + (CClosure.create_tab ()) (CClosure.inject (EConstr.Unsafe.to_constr t))) with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") |