From 90b61424761c5ba1ddbecf20c29d78b485584ae7 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Mon, 12 Dec 2016 14:18:48 +0100
Subject: Extend Fast_typeops to be a replacement for Typeops

This brings the fix in cad44fc for #2996 to the copy of
Fast_typeops.check_hyps_inclusion.

Fast_typeops.constant_type checks the universe constraints instead of
outputting them. Since everyone who used Typeops.constant_type just
discarded the constraints they've been switched to constant_type_in
which should be the same in Fast_typeops and Typeops.

There are some small differences in the interfaces:
- Typeops.type_of_projection <->
  Fast_typeops.type_of_projection_constant to avoid collision with the
  internally used type_of_projection (which gives the type of [Proj(p,c)]).
- check_hyps_inclusion takes [('a -> constr)] and ['a] instead of
  [constr] for reporting errors.
---
 plugins/extraction/extraction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a980a43f53..33fab74e13 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -258,7 +258,7 @@ let rec extract_type env db j c args =
     | Const (kn,u as c) ->
 	let r = ConstRef kn in
 	let cb = lookup_constant kn env in
-	let typ,_ = Typeops.type_of_constant env c in
+        let typ = Typeops.type_of_constant_in env c in (* FIXME constraints *)
 	(match flag_of_type env typ with
 	   | (Logic,_) -> assert false (* Cf. logical cases above *)
 	   | (Info, TypeScheme) ->
-- 
cgit v1.2.3


From 90b6969c467f097a4d7da0140e1351ef98d6401d Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Sat, 28 Jan 2017 14:11:50 +0100
Subject: Remove useless comments

---
 plugins/extraction/extraction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 33fab74e13..2b19c2805f 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -258,7 +258,7 @@ let rec extract_type env db j c args =
     | Const (kn,u as c) ->
 	let r = ConstRef kn in
 	let cb = lookup_constant kn env in
-        let typ = Typeops.type_of_constant_in env c in (* FIXME constraints *)
+        let typ = Typeops.type_of_constant_in env c in
 	(match flag_of_type env typ with
 	   | (Logic,_) -> assert false (* Cf. logical cases above *)
 	   | (Info, TypeScheme) ->
-- 
cgit v1.2.3