diff options
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/cbytegen.mli | 1 | ||||
-rw-r--r-- | kernel/cemitcodes.ml | 1 | ||||
-rw-r--r-- | kernel/closure.ml | 18 | ||||
-rw-r--r-- | kernel/declareops.mli | 1 | ||||
-rw-r--r-- | kernel/fast_typeops.mli | 5 | ||||
-rw-r--r-- | kernel/indtypes.ml | 1 | ||||
-rw-r--r-- | kernel/inductive.ml | 7 | ||||
-rw-r--r-- | kernel/names.ml | 1 | ||||
-rw-r--r-- | kernel/nativecode.ml | 1 | ||||
-rw-r--r-- | kernel/nativelambda.mli | 1 | ||||
-rw-r--r-- | kernel/nativelibrary.ml | 1 | ||||
-rw-r--r-- | kernel/opaqueproof.mli | 1 | ||||
-rw-r--r-- | kernel/reduction.ml | 8 | ||||
-rw-r--r-- | kernel/term_typing.ml | 5 | ||||
-rw-r--r-- | kernel/term_typing.mli | 1 | ||||
-rw-r--r-- | kernel/vconv.ml | 2 |
16 files changed, 0 insertions, 55 deletions
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index eab36d8b2..8fb6601a9 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -1,4 +1,3 @@ -open Names open Cbytecodes open Cemitcodes open Term diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 3c9692a5c..9ecae2b36 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -10,7 +10,6 @@ machine, Oct 2004 *) (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) -open Names open Term open Cbytecodes open Copcodes diff --git a/kernel/closure.ml b/kernel/closure.ml index f06b13d8d..6824c399e 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -771,24 +771,6 @@ let drop_parameters depth n argstk = (* we know that n < stack_args_size(argstk) (if well-typed term) *) anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor") - -let rec get_parameters depth n argstk = - match argstk with - Zapp args::s -> - let q = Array.length args in - if n > q then Array.append args (get_parameters depth (n-q) s) - else if Int.equal n q then [||] - else Array.sub args 0 n - | Zshift(k)::s -> - get_parameters (depth-k) n s - | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *) - if Int.equal n 0 then [||] - else raise Not_found (* Trying to eta-expand a partial application..., should do - eta expansion first? *) - | _ -> assert false - (* strip_update_shift_app only produces Zapp and Zshift items *) - - (** [eta_expand_ind_stack env ind c s t] computes stacks correspoding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 47a82cc6c..ce65af975 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -9,7 +9,6 @@ open Declarations open Mod_subst open Univ -open Context (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli index 4c2c92ccf..90d9c55f1 100644 --- a/kernel/fast_typeops.mli +++ b/kernel/fast_typeops.mli @@ -6,13 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Univ open Term -open Context open Environ -open Entries -open Declarations (** {6 Typing functions (not yet tagged as safe) } diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 99d9f52c9..ea575e1e0 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -654,7 +654,6 @@ let used_section_variables env inds = keep_hyps env ids let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) -let rel_appvect n m = rel_vect n (List.length m) exception UndefinableExpansion diff --git a/kernel/inductive.ml b/kernel/inductive.ml index bb57ad256..6b4dd536a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -447,13 +447,6 @@ type subterm_spec = let eq_wf_paths = Rtree.equal Declareops.eq_recarg -let pp_recarg = function - | Norec -> Pp.str "Norec" - | Mrec i -> Pp.str ("Mrec "^MutInd.to_string (fst i)) - | Imbr i -> Pp.str ("Imbr "^MutInd.to_string (fst i)) - -let pp_wf_paths = Rtree.pp_tree pp_recarg - let inter_recarg r1 r2 = match r1, r2 with | Norec, Norec -> Some r1 | Mrec i1, Mrec i2 diff --git a/kernel/names.ml b/kernel/names.ml index b349ccb00..4ccf5b60a 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -571,7 +571,6 @@ let constr_modpath (ind,_) = ind_modpath ind let ith_mutual_inductive (mind, _) i = (mind, i) let ith_constructor_of_inductive ind i = (ind, i) -let ith_constructor_of_pinductive (ind,u) i = ((ind,i),u) let inductive_of_constructor (ind, i) = ind let index_of_constructor (ind, i) = i diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 1a4a4b54d..ada7ae737 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -12,7 +12,6 @@ open Context open Declarations open Util open Nativevalues -open Primitives open Nativeinstr open Nativelambda open Pre_env diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 6a97edc40..ccf2888b5 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -8,7 +8,6 @@ open Names open Term open Pre_env -open Nativevalues open Nativeinstr (** This file defines the lambda code generation phase of the native compiler *) diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 914f577e2..0b8662ff0 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -12,7 +12,6 @@ open Environ open Mod_subst open Modops open Nativecode -open Nativelib (** This file implements separate compilation for libraries in the native compiler *) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 87cebd62f..0609c8517 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -9,7 +9,6 @@ open Names open Term open Mod_subst -open Int (** This module implements the handling of opaque proof terms. Opauqe proof terms are special since: diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 4153b323b..b09367dd9 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -28,14 +28,6 @@ open Esubst let left2right = ref false -let conv_key k = - match k with - VarKey id -> - VarKey id - | ConstKey (cst,_) -> - ConstKey cst - | RelKey n -> RelKey n - let rec is_empty_stack = function [] -> true | Zupdate _::s -> is_empty_stack s diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index a3441aa3e..b54511e40 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -15,7 +15,6 @@ open Errors open Util open Names -open Univ open Term open Context open Declarations @@ -101,10 +100,6 @@ let hcons_j j = let feedback_completion_typecheck = Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) - -let subst_instance_j s j = - { uj_val = Vars.subst_univs_level_constr s j.uj_val; - uj_type = Vars.subst_univs_level_constr s j.uj_type } let infer_declaration env kn dcl = match dcl with diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 696fc3d2d..1b54b1ea1 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -8,7 +8,6 @@ open Names open Term -open Univ open Environ open Declarations open Entries diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 80b15f8ba..29315b0a9 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -42,8 +42,6 @@ let conv_vect fconv vect1 vect2 cu = let infos = ref (create_clos_infos betaiotazeta Environ.empty_env) -let eq_table_key = Names.eq_table_key eq_constant - let rec conv_val env pb k v1 v2 cu = if v1 == v2 then cu else conv_whd env pb k (whd_val v1) (whd_val v2) cu |