aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2016-12-12 14:18:48 +0100
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2016-12-12 14:18:48 +0100
commit90b61424761c5ba1ddbecf20c29d78b485584ae7 (patch)
tree5143571cdc885ebae5b0754efff18114644a8be8 /plugins/extraction
parentad768e435a736ca51ac79a575967b388b34918c7 (diff)
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.
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/extraction.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a980a43f5..33fab74e1 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) ->