Merge branch 'trunk' into located_switch

9 files changed, 10 insertions, 54 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index 95a9ea78b1..5cadfe7b94 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 cef1d31a68..b8294e7958 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 1fe02c8b60..ad93146d55 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 6bea3c91a7..09bf2826c0 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 c4ffc141ff..8f23a38afc 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/subtyping.ml b/checker/subtyping.ml
index 7eae9b8310..a290b240d8 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -113,7 +113,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   in
   let check_inductive_type env t1 t2 =
 
-    (* Due to sort-polymorphism in inductive types, the conclusions of
+    (* Due to template polymorphism, the conclusions of
        t1 and t2, if in Type, are generated as the least upper bounds
        of the types of the constructors.
 
diff --git a/checker/term.ml b/checker/term.ml
index 591348cb69..24e6008d34 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* This module instantiates the structure of generic deBruijn terms to Coq *)
+(* This module instantiates the structure of generic de Bruijn terms to Coq *)
 
 open CErrors
 open Util
@@ -94,7 +94,7 @@ let closedn n c =
   in
   try closed_rec n c; true with LocalOccur -> false
 
-(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+(* [closed0 M] is true iff [M] is a (de Bruijn) closed term *)
 
 let closed0 = closedn 0
 
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 173e19ce1b..1396d56df3 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
@@ -278,13 +275,11 @@ let rec execute env cstr =
 	let j =
 	  match f with
 	    | Ind ind ->
-		(* Sort-polymorphism of inductive types *)
 		judge_of_inductive_knowing_parameters env ind jl
 	    | Const cst ->
-		(* Sort-polymorphism of constant *)
 		judge_of_constant_knowing_parameters env cst jl
 	    | _ ->
-		(* No sort-polymorphism *)
+		(* No template polymorphism *)
 		execute env f
 	in
         let jl = Array.map2 (fun c ty -> c,ty) args jl in
diff --git a/checker/univ.ml b/checker/univ.ml
index 668f3a0584..fb1a0faa78 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