diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 399264859..ee5acffd9 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -157,7 +157,7 @@ sig rawconstr -> unsafe_type_judgment val pretype_gen : - evar_defs ref -> env -> + evar_defs ref -> env -> var_map * (identifier * identifier option) list -> typing_constraint -> rawconstr -> constr @@ -667,11 +667,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct | IsType -> (pretype_type empty_valcon env evdref lvar c).utj_val in let evd,_ = consider_remaining_unif_problems env !evdref in - let evd = nf_evar_defs evd in let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in - let c' = nf_evar (evars_of evd) c' in evdref := evd; - c' + nf_evar (evars_of evd) c' (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage |