diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cbytegen.ml | 2 | ||||
| -rw-r--r-- | kernel/environ.ml | 4 | ||||
| -rw-r--r-- | kernel/mod_subst.ml | 2 | ||||
| -rw-r--r-- | kernel/term.ml | 6 | ||||
| -rw-r--r-- | kernel/typeops.ml | 2 |
5 files changed, 8 insertions, 8 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index d6b3a9596c..7a40a40297 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -220,7 +220,7 @@ let pos_rel i r sz = (* non-terminating instruction (branch, raise, return, appterm) *) (* in front of it. *) -let rec discard_dead_code cont = cont +let discard_dead_code cont = cont (*function [] -> [] | (Klabel _ | Krestart ) :: _ as cont -> cont diff --git a/kernel/environ.ml b/kernel/environ.ml index 2c723a8344..f1adb53406 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -317,7 +317,7 @@ let compile_constant_body = Cbytegen.compile_constant_body exception Hyp_not_found -let rec apply_to_hyp (ctxt,vals) id f = +let apply_to_hyp (ctxt,vals) id f = let rec aux rtail ctxt vals = match ctxt, vals with | (idc,c,ct as d)::ctxt, v::vals -> @@ -330,7 +330,7 @@ let rec apply_to_hyp (ctxt,vals) id f = | _, _ -> assert false in aux [] ctxt vals -let rec apply_to_hyp_and_dependent_on (ctxt,vals) id f g = +let apply_to_hyp_and_dependent_on (ctxt,vals) id f g = let rec aux ctxt vals = match ctxt,vals with | (idc,c,ct as d)::ctxt, v::vals -> diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 7c0b14dce3..a9d4d88325 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -147,7 +147,7 @@ let mind_in_delta mind resolver = kn_in_delta (user_mind mind) resolver let mp_of_delta resolve mp = try Deltamap.find_mp mp resolve with Not_found -> mp -let rec find_prefix resolve mp = +let find_prefix resolve mp = let rec sub_mp = function | MPdot(mp,l) as mp_sup -> (try Deltamap.find_mp mp_sup resolve diff --git a/kernel/term.ml b/kernel/term.ml index 9a25de1bcf..16649b1815 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -108,6 +108,8 @@ type ('constr, 'types) kind_of_term = -rectypes of the Caml compiler to be set *) type constr = (constr,constr) kind_of_term +type strategy = types option + type existential = existential_key * constr array type rec_declaration = name array * constr array * constr array type fixpoint = (int array * int) * rec_declaration @@ -429,7 +431,7 @@ let rec under_casts f c = match kind_of_term c with (******************************************************************) (* flattens application lists throwing casts in-between *) -let rec collapse_appl c = match kind_of_term c with +let collapse_appl c = match kind_of_term c with | App (f,cl) -> let rec collapse_rec f cl2 = match kind_of_term (strip_outer_cast f) with @@ -647,8 +649,6 @@ let rec constr_ord m n= type types = constr -type strategy = types option - type named_declaration = identifier * constr option * types type rel_declaration = name * constr option * types diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 9487b6d393..608bcc886c 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -95,7 +95,7 @@ let judge_of_variable env id = (* Checks if a context of variable can be instantiated by the variables of the current env *) (* TODO: check order? *) -let rec check_hyps_inclusion env sign = +let check_hyps_inclusion env sign = Sign.fold_named_context (fun (id,_,ty1) () -> let ty2 = named_type id env in |