diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 2b7199a763..7644b49ceb 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i*) -open API open Util open Names open Term @@ -296,7 +295,11 @@ let rec extract_type env db j c args = | Ind ((kn,i),u) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in extract_type_app env db (IndRef (kn,i),s) args - | Case _ | Fix _ | CoFix _ | Proj _ -> Tunknown + | Proj (p,t) -> + (* Let's try to reduce, if it hasn't already been done. *) + if Projection.unfolded p then Tunknown + else extract_type env db j (Term.mkProj (Projection.unfold p, t)) args + | Case _ | Fix _ | CoFix _ -> Tunknown | _ -> assert false (*s Auxiliary function dealing with type application. @@ -519,7 +522,7 @@ and mlt_env env r = match r with match lookup_typedef kn cb with | Some _ as o -> o | None -> - let typ = Typeops.type_of_constant_type env cb.const_type + let typ = cb.const_type (* FIXME not sure if we should instantiate univs here *) in match flag_of_type env typ with | Info,TypeScheme -> @@ -544,7 +547,7 @@ let record_constant_type env kn opt_typ = | Some schema -> schema | None -> let typ = match opt_typ with - | None -> Typeops.type_of_constant_type env cb.const_type + | None -> cb.const_type | Some typ -> typ in let mlt = extract_type env [] 1 typ [] in @@ -970,7 +973,7 @@ let extract_fixpoint env vkn (fi,ti,ci) = let extract_constant env kn cb = let r = ConstRef kn in - let typ = Typeops.type_of_constant_type env cb.const_type in + let typ = 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 @@ -1026,7 +1029,7 @@ let extract_constant env kn cb = let extract_constant_spec env kn cb = let r = ConstRef kn in - let typ = Typeops.type_of_constant_type env cb.const_type in + let typ = cb.const_type in try match flag_of_type env typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) |