diff options
Diffstat (limited to 'checker')
-rw-r--r-- | checker/checker.ml | 4 | ||||
-rw-r--r-- | checker/closure.ml | 16 | ||||
-rw-r--r-- | checker/declarations.ml | 13 | ||||
-rw-r--r-- | checker/include | 2 | ||||
-rw-r--r-- | checker/inductive.ml | 9 | ||||
-rw-r--r-- | checker/typeops.ml | 3 | ||||
-rw-r--r-- | checker/univ.ml | 7 |
7 files changed, 6 insertions, 48 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index 95a9ea78b..5cadfe7b9 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -221,7 +221,7 @@ let where = function | Some s -> if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) -let rec explain_exn = function +let explain_exn = function | Stream.Failure -> hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.") | Stream.Error txt -> @@ -354,7 +354,7 @@ let parse_args argv = | "-norec" :: [] -> usage () | "-silent" :: rem -> - Flags.make_silent true; parse rem + Flags.quiet := true; parse rem | s :: _ when s<>"" && s.[0]='-' -> fatal_error (str "Unknown option " ++ str s) false diff --git a/checker/closure.ml b/checker/closure.ml index cef1d31a6..b8294e795 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -651,22 +651,6 @@ let drop_parameters depth n argstk = (** Projections and eta expansion *) -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 *) - let eta_expand_ind_stack env ind m s (f, s') = let mib = lookup_mind (fst ind) env in match mib.mind_record with diff --git a/checker/declarations.ml b/checker/declarations.ml index 1fe02c8b6..ad93146d5 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -6,6 +6,7 @@ open Term (** Substitutions, code imported from kernel/mod_subst *) module Deltamap = struct + [@@@ocaml.warning "-32-34"] type t = delta_resolver let empty = MPmap.empty, KNmap.empty let is_empty (mm, km) = MPmap.is_empty mm && KNmap.is_empty km @@ -25,6 +26,7 @@ end let empty_delta_resolver = Deltamap.empty module Umap = struct + [@@@ocaml.warning "-32-34"] type 'a t = 'a umap_t let empty = MPmap.empty, MBImap.empty let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2 @@ -461,13 +463,6 @@ let is_opaque cb = match cb.const_body with let opaque_univ_context cb = force_lazy_constr_univs cb.const_body -let subst_rel_declaration sub (id,copt,t as x) = - let copt' = Option.smartmap (subst_mps sub) copt in - let t' = subst_mps sub t in - if copt == copt' && t == t' then x else (id,copt',t') - -let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) - let subst_recarg sub r = match r with | Norec -> r | (Mrec(kn,i)|Imbr (kn,i)) -> let kn' = subst_ind sub kn in @@ -515,10 +510,6 @@ let subst_decl_arity f g sub ar = if x' == x then ar else TemplateArity x' -let map_decl_arity f g = function - | RegularArity a -> RegularArity (f a) - | TemplateArity a -> TemplateArity (g a) - let subst_rel_declaration sub = Term.map_rel_decl (subst_mps sub) diff --git a/checker/include b/checker/include index 6bea3c91a..09bf2826c 100644 --- a/checker/include +++ b/checker/include @@ -116,7 +116,7 @@ let prsub s = #install_printer prsub;;*) Checker.init_with_argv [|"";"-coqlib";"."|];; -Flags.make_silent false;; +Flags.quiet := false;; Flags.debug := true;; Sys.catch_break true;; diff --git a/checker/inductive.ml b/checker/inductive.ml index c4ffc141f..8f23a38af 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -149,7 +149,7 @@ let remember_subst u subst = (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) -let rec make_subst env = +let make_subst env = let rec make subst = function | LocalDef _ :: sign, exp, args -> make subst (sign, exp, args) @@ -436,13 +436,6 @@ let eq_recarg r1 r2 = match r1, r2 with let eq_wf_paths = Rtree.equal 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/checker/typeops.ml b/checker/typeops.ml index 173e19ce1..02d801741 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -85,9 +85,6 @@ let type_of_constant_knowing_parameters env cst paramtyps = let type_of_constant_type env t = type_of_constant_type_knowing_parameters env t [||] -let type_of_constant env cst = - type_of_constant_knowing_parameters env cst [||] - let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp = let _cb = try lookup_constant kn env diff --git a/checker/univ.ml b/checker/univ.ml index 668f3a058..fb1a0faa7 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -87,7 +87,6 @@ module HList = struct val exists : (elt -> bool) -> t -> bool val for_all : (elt -> bool) -> t -> bool val for_all2 : (elt -> elt -> bool) -> t -> t -> bool - val remove : elt -> t -> t val to_list : t -> elt list end @@ -128,12 +127,6 @@ module HList = struct | Nil -> [] | Cons (x, _, l) -> x :: to_list l - let rec remove x = function - | Nil -> nil - | Cons (y, _, l) -> - if H.eq x y then l - else cons y (remove x l) - end end |