diff options
-rw-r--r-- | kernel/sorts.ml | 2 | ||||
-rw-r--r-- | library/universes.ml | 13 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 12 | ||||
-rw-r--r-- | plugins/setoid_ring/Field_theory.v | 4 |
4 files changed, 23 insertions, 8 deletions
diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 3ebd06dd8..bfcdc0b4d 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -47,10 +47,12 @@ let equal s1 s2 = Int.equal (compare s1 s2) 0 let is_prop = function | Prop Null -> true + | Type u when Universe.equal Universe.type0m u -> true | _ -> false let is_set = function | Prop Pos -> true + | Type u when Universe.equal Universe.type0 u -> true | _ -> false let is_small = function diff --git a/library/universes.ml b/library/universes.ml index 6799a99e5..dd5331fa7 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -691,13 +691,22 @@ let restrict_universe_context (univs,csts) s = (* Universes that are not necessary to typecheck the term. E.g. univs introduced by tactics and not used in the proof term. *) let diff = LSet.diff univs s in + let is_useless l r = + let lmem = LSet.mem l diff + and rmem = LSet.mem r diff in + lmem && rmem + (* if lmem then *) + (* rmem || not (LSet.mem r univs) *) + (* else *) + (* rmem && not (LSet.mem l s) *) + in let (univscstrs, csts) = Constraint.fold (fun (l,d,r as c) (univs, csts) -> - if LSet.mem l diff && LSet.mem r diff then (univs, csts) + if is_useless l r then (univs, csts) else (LSet.add l (LSet.add r univs), Constraint.add c csts)) csts (LSet.empty, Constraint.empty) - in (LSet.union s (LSet.inter univs univscstrs), csts) + in (LSet.inter univs (LSet.union s univscstrs), csts) let simplify_universe_context (univs,csts) = let uf = UF.create () in 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) diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 10d54d228..ad7fbd871 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -588,13 +588,13 @@ Qed. (** Smart constructors for polynomial expression, with reduction of constants *) -Time Definition NPEadd e1 e2 := +Definition NPEadd e1 e2 := match e1, e2 with | PEc c1, PEc c2 => PEc (c1 + c2) | PEc c, _ => if (c =? 0)%coef then e2 else e1 + e2 | _, PEc c => if (c =? 0)%coef then e1 else e1 + e2 (* Peut t'on factoriser ici ??? *) - | _, _ => (@PEadd C e1 e2) + | _, _ => (e1 + e2) end%poly. Infix "++" := NPEadd (at level 60, right associativity). |