From 8361be1d785f8588d2d3c2a0df7a1d9239bae5a1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 9 Oct 2018 16:45:34 +0200
Subject: Remove a few circumvolutions around parameters of inductive entries

---
 interp/discharge.ml | 11 +----------
 1 file changed, 1 insertion(+), 10 deletions(-)

(limited to 'interp')

diff --git a/interp/discharge.ml b/interp/discharge.ml
index 0e44a8b467..21b2e85e8f 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -8,8 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Names
-open CErrors
 open Util
 open Term
 open Constr
@@ -17,17 +15,10 @@ open Vars
 open Declarations
 open Cooking
 open Entries
-open Context.Rel.Declaration
 
 (********************************)
 (* Discharging mutual inductive *)
 
-let detype_param =
-  function
-  | LocalAssum (Name id, p) -> id, LocalAssumEntry p
-  | LocalDef (Name id, p,_) -> id, LocalDefEntry p
-  | _ -> anomaly (Pp.str "Unnamed inductive local variable.")
-
 (* Replace
 
      Var(y1)..Var(yq):C1..Cq |- Ij:Bj
@@ -57,7 +48,7 @@ let abstract_inductive decls nparamdecls inds =
 (* To be sure to be the same as before, should probably be moved to process_inductive *)
   let params' = let (_,arity,_,_,_) = List.hd inds' in
 		let (params,_) = decompose_prod_n_assum nparamdecls' arity in
-                List.map detype_param params
+    params
   in
   let ind'' =
   List.map
-- 
cgit v1.2.3