From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 toplevel/discharge.ml | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

(limited to 'toplevel/discharge.ml')

diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 61573091..e24d5e74 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -7,22 +7,23 @@
 (************************************************************************)
 
 open Names
-open Errors
+open CErrors
 open Util
-open Context
 open Term
 open Vars
-open Entries
 open Declarations
 open Cooking
+open Entries
+open Context.Rel.Declaration
 
 (********************************)
 (* Discharging mutual inductive *)
 
-let detype_param = function
-  | (Name id,None,p) -> id, LocalAssum p
-  | (Name id,Some p,_) -> id, LocalDef p
-  | (Anonymous,_,_) -> anomaly (Pp.str "Unnamed inductive local variable")
+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
 
@@ -37,8 +38,8 @@ let detype_param = function
 
 let abstract_inductive hyps nparams inds =
   let ntyp = List.length inds in
-  let nhyp = named_context_length hyps in
-  let args = instance_from_named_context (List.rev hyps) in
+  let nhyp = Context.Named.length hyps in
+  let args = Context.Named.to_instance (List.rev hyps) in
   let args = Array.of_list args in
   let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in
   let inds' =
@@ -53,7 +54,7 @@ let abstract_inductive hyps nparams 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 nparams' arity in
-		  List.map detype_param params
+                List.map detype_param params
   in
   let ind'' =
   List.map
@@ -100,7 +101,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
 	   Array.to_list mip.mind_consnames,
 	   Array.to_list lc))
       mib.mind_packets in
-  let sechyps' = map_named_context (expmod_constr modlist) sechyps in
+  let sechyps' = Context.Named.map (expmod_constr modlist) sechyps in
   let (params',inds') = abstract_inductive sechyps' nparams inds in
   let abs_ctx = Univ.instantiate_univ_context abs_ctx in
   let univs = Univ.UContext.union abs_ctx univs in
@@ -115,5 +116,5 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
     mind_entry_inds = inds';
     mind_entry_polymorphic = mib.mind_polymorphic;
     mind_entry_private = mib.mind_private;
-    mind_entry_universes = univs
+    mind_entry_universes = univs;
   }
-- 
cgit v1.2.3