From ce11f55e27c8e4f98384aacd61ee67c593340195 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 2 May 2014 11:33:34 +0200 Subject: Fix extraction taking a type in the wrong environment. Fix restriction of universe contexts to not forget about potentially useful constraints. --- plugins/extraction/extraction.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'plugins/extraction/extraction.ml') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index f9dfd1fa4..0ddc7c006 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -76,7 +76,7 @@ let rec flag_of_type env t : flag = let t = whd_betadeltaiota env none t in match kind_of_term t with | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c - | Sort (Prop Null) -> (Logic,TypeScheme) + | Sort s when Sorts.is_prop s -> (Logic,TypeScheme) | Sort _ -> (Info,TypeScheme) | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default) @@ -206,7 +206,11 @@ let oib_equal o1 o2 = match o1.mind_arity, o2.mind_arity with | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} -> eq_constr c1 c2 && Sorts.equal s1 s2 - | _ -> false + | TemplateArity p1, TemplateArity p2 -> + let eq o1 o2 = Option.equal Univ.Universe.equal o1 o2 in + List.equal eq p1.template_param_levels p2.template_param_levels && + Univ.Universe.equal p1.template_level p2.template_level + | _, _ -> false end && Array.equal Id.equal o1.mind_consnames o2.mind_consnames @@ -976,7 +980,7 @@ let extract_fixpoint env vkn (fi,ti,ci) = let extract_constant env kn cb = let r = ConstRef kn in - let typ = Global.type_of_global_unsafe r in + let typ = Typeops.type_of_constant_type env cb.const_type in let warn_info () = if not (is_custom r) then add_info_axiom r in let warn_log () = if not (constant_has_body cb) then add_log_axiom r in @@ -1023,7 +1027,7 @@ let extract_constant env kn cb = let extract_constant_spec env kn cb = let r = ConstRef kn in - let typ = Global.type_of_global_unsafe r in + let typ = Typeops.type_of_constant_type env cb.const_type in match flag_of_type env typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) | (Logic, Default) -> Sval (r, Tdummy Kother) -- cgit v1.2.3