Fix extraction taking a type in the wrong environment.

Fix restriction of universe contexts to not forget about potentially useful
constraints.

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).