diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 15 |
1 files changed, 1 insertions, 14 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5b4e8e7cf..db492c026 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -695,14 +695,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct let ise_pretype_gen fail_evar sigma env lvar kind c = let evdref = ref (Evd.create_evar_defs sigma) in let c = pretype_gen evdref env lvar kind c in -(* let evd,_ = consider_remaining_unif_problems env !evdref in *) -(* let evd = nf_evar_defs evd in *) -(* let c = nf_evar (evars_of evd) c in *) -(* let evd = undefined_evars evd in *) -(* let evd = Typeclasses.resolve_typeclasses env sigma evd in *) -(* let c = nf_evar (evars_of evd) c in *) let evd,_ = consider_remaining_unif_problems env !evdref in - if fail_evar then check_evars env (Evd.evars_of evd) evd c; + if fail_evar then check_evars env Evd.empty evd c; evd, c (** Entry points of the high-level type synthesis algorithm *) @@ -721,13 +715,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct let understand_tcc_evars evdref env kind c = pretype_gen evdref env ([],[]) kind c -(* let c = pretype_gen evdref env ([],[]) kind c in *) -(* evdref := nf_evar_defs !evdref; *) -(* let c = nf_evar (evars_of !evdref) c in *) -(* let evd = undefined_evars !evdref in *) -(* let evd = Typeclasses.resolve_typeclasses env (evars_of evd) !evdref in *) -(* evdref := evd; *) -(* nf_evar (evars_of evd) c *) let understand_tcc sigma env ?expected_type:exptyp c = let evd, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in |