diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 27 |
1 files changed, 14 insertions, 13 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c114a922c..83594466e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -696,12 +696,13 @@ 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 - evdref := evd; c' + evdref := evd; + nf_isevar !evdref c' let pretype_gen evdref env lvar kind c = let c = pretype_gen_aux evdref env lvar kind c in evdref := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !evdref; - nf_evar (evars_of !evdref) c + nf_isevar !evdref c (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage @@ -730,7 +731,7 @@ 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 c = pretype_gen_aux evdref env lvar kind c in let evd,_ = consider_remaining_unif_problems env !evdref in if fail_evar then let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in @@ -755,17 +756,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct let understand_tcc_evars evdref env kind c = pretype_gen evdref env ([],[]) kind c - + let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = let evd, t = - if resolve_classes then - ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c - else - let evdref = ref (Evd.create_evar_defs sigma) in - let c = pretype_gen_aux evdref env ([],[]) (OfType exptyp) c in - !evdref, nf_isevar !evdref c - in - Evd.evars_of evd, t + let evdref = ref (Evd.create_evar_defs sigma) in + let c = + if resolve_classes then + pretype_gen evdref env ([],[]) (OfType exptyp) c + else + pretype_gen_aux evdref env ([],[]) (OfType exptyp) c + in !evdref, c + in Evd.evars_of evd, t end - + module Default : S = Pretyping_F(Coercion.Default) |