diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-19 13:13:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-19 13:13:20 +0100 |
commit | 2155252cd74c3a2d0dc0bde716ef70b1f86b8085 (patch) | |
tree | 20313deb80e22ea9088f1e6ba0bb9336f3718b25 /contrib/xml/cic2acic.ml | |
parent | 06746919eadeeb430bfb464d83847f982ea78540 (diff) | |
parent | a0a94c1340a63cdb824507b973393882666ba52a (diff) |
Merge commit 'upstream/8.2-1+dfsg'
Diffstat (limited to 'contrib/xml/cic2acic.ml')
-rw-r--r-- | contrib/xml/cic2acic.ml | 6 |
1 files changed, 3 insertions, 3 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} |