diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-07-12 18:46:08 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-09-29 14:13:24 +0200 |
| commit | af051436672561b4c15e07dfe4f9cee93f0741a4 (patch) | |
| tree | 59cc6650d525ffb7c2aedda1a8396dc12a5d88f8 /plugins/extraction | |
| parent | a6832ccfacd9c105b23a9a77dadc3202f7af26fc (diff) | |
Extraction: ignore some useless stuff about universes
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extraction.ml | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 312c2eab3..a980a43f5 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -371,8 +371,7 @@ and extract_really_ind env kn mib = let packets = Array.mapi (fun i mip -> - let (ind,u), ctx = - Universes.fresh_inductive_instance env (kn,i) in + let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in let ar = Inductive.type_of_inductive env ((mib,mip),u) in let info = (fst (flag_of_type env ar) = Info) in let s,v = if info then type_sign_vl env ar else [],[] in @@ -591,10 +590,10 @@ let rec extract_term env mle mlt c args = with NotDefault d -> let mle' = Mlenv.push_std_type mle (Tdummy d) in ast_pop (extract_term env' mle' mlt c2 args')) - | Const (kn,u) -> - extract_cst_app env mle mlt kn u args - | Construct (cp,u) -> - extract_cons_app env mle mlt cp u args + | Const (kn,_) -> + extract_cst_app env mle mlt kn args + | Construct (cp,_) -> + extract_cons_app env mle mlt cp args | Proj (p, c) -> let term = Retyping.expand_projection env (Evd.from_env env) p c [] in extract_term env mle mlt term args @@ -645,7 +644,7 @@ and make_mlargs env e s args typs = (*s Extraction of a constant applied to arguments. *) -and extract_cst_app env mle mlt kn u args = +and extract_cst_app env mle mlt kn args = (* First, the [ml_schema] of the constant, in expanded version. *) let nb,t = record_constant_type env kn None in let schema = nb, expand env t in @@ -718,7 +717,7 @@ and extract_cst_app env mle mlt kn u args = they are fixed, and thus are not used for the computation. \end{itemize} *) -and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args = +and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = (* First, we build the type of the constructor, stored in small pieces. *) let mi = extract_ind env kn in let params_nb = mi.ind_nparams in |