diff options
Diffstat (limited to 'contrib/xml')
| -rw-r--r-- | contrib/xml/cic2acic.ml | 6 | ||||
| -rw-r--r-- | contrib/xml/doubleTypeInference.ml | 8 |
2 files changed, 7 insertions, 7 deletions
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index c62db00b..13e5e6d5 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -245,9 +245,9 @@ let typeur sigma metamap = let Inductiveops.IndType(_,realargs) = try Inductiveops.find_rectype env sigma (type_of env c) with Not_found -> Util.anomaly "type_of: Bad recursive type" in - let t = Reductionops.whd_beta (T.applist (p, realargs)) in + let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with - | T.Prod _ -> Reductionops.whd_beta (T.applist (t, [c])) + | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c])) | _ -> t) | T.Lambda (name,c1,c2) -> T.mkProd (name, c1, type_of (Environ.push_rel (name,None,c1) env) c2) @@ -390,7 +390,7 @@ Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-ty (* We need to refresh the universes because we are doing *) (* type inference on an already inferred type. *) {D.synthesized = - Reductionops.nf_beta + Reductionops.nf_beta evar_map (CPropRetyping.get_type_of env evar_map (Termops.refresh_universes tt)) ; D.expected = None} diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index de8c540c..17d1d5da 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -163,7 +163,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = | hj::restjl -> match T.kind_of_term (Reduction.whd_betadeltaiota env typ) with T.Prod (_,c1,c2) -> - (Some (Reductionops.nf_beta c1)) :: + (Some (Reductionops.nf_beta sigma c1)) :: (aux (T.subst1 hj c2) restjl) | _ -> assert false in @@ -183,7 +183,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = | Some ety -> match T.kind_of_term (Reduction.whd_betadeltaiota env ety) with T.Prod (_,_,expected_target_type) -> - Some (Reductionops.nf_beta expected_target_type) + Some (Reductionops.nf_beta sigma expected_target_type) | _ -> assert false in let j' = execute env1 sigma c2 expectedc2type in @@ -214,14 +214,14 @@ let double_type_of env sigma cstr expectedty subterms_to_types = Typeops.judge_of_letin env name j1 j2 j3 | T.Cast (c,k,t) -> - let cj = execute env sigma c (Some (Reductionops.nf_beta t)) in + let cj = execute env sigma c (Some (Reductionops.nf_beta sigma t)) in let tj = execute env sigma t None in let tj = type_judgment env sigma tj in let j, _ = Typeops.judge_of_cast env cj k tj in j in let synthesized = E.j_type judgement in - let synthesized' = Reductionops.nf_beta synthesized in + let synthesized' = Reductionops.nf_beta sigma synthesized in let types,res = match expectedty with None -> |