From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 checker/term.ml | 41 ++++++++++++++++-------------------------
 1 file changed, 16 insertions(+), 25 deletions(-)

(limited to 'checker/term.ml')

diff --git a/checker/term.ml b/checker/term.ml
index 61369586..ab40b6fa 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: term.ml 10098 2007-08-27 11:41:08Z herbelin $ *)
-
 (* This module instantiates the structure of generic deBruijn terms to Coq *)
 
 open Util
@@ -31,15 +29,15 @@ type case_printing =
   { ind_nargs : int; (* length of the arity of the inductive type *)
     style     : case_style }
 type case_info =
-  { ci_ind        : inductive;
-    ci_npar       : int;
-    ci_cstr_nargs : int array; (* number of real args of each constructor *)
-    ci_pp_info    : case_printing (* not interpreted by the kernel *)
+  { ci_ind         : inductive;
+    ci_npar        : int;
+    ci_cstr_ndecls : int array; (* number of pattern var of each constructor *)
+    ci_pp_info     : case_printing (* not interpreted by the kernel *)
   }
 let val_ci =
   let val_cstyle = val_enum "case_style" 5 in
-  let val_cprint = val_tuple "case_printing" [|val_int;val_cstyle|] in
-  val_tuple "case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
+  let val_cprint = val_tuple ~name:"case_printing" [|val_int;val_cstyle|] in
+  val_tuple ~name:"case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
 
 (* Sorts. *)
 
@@ -73,13 +71,14 @@ type 'constr pfixpoint =
 type 'constr pcofixpoint =
     int * 'constr prec_declaration
 
-let val_evar f = val_tuple "pexistential" [|val_int;val_array f|]
+let val_evar f = val_tuple ~name:"pexistential" [|val_int;val_array f|]
 let val_prec f =
-  val_tuple "prec_declaration"[|val_array val_name; val_array f; val_array f|]
+  val_tuple ~name:"prec_declaration"
+    [|val_array val_name; val_array f; val_array f|]
 let val_fix f =
-  val_tuple"pfixpoint"
-    [|val_tuple"fix2"[|val_array val_int;val_int|];val_prec f|]
-let val_cofix f = val_tuple"pcofixpoint"[|val_int;val_prec f|]
+  val_tuple ~name:"pfixpoint"
+    [|val_tuple~name:"fix2"[|val_array val_int;val_int|];val_prec f|]
+let val_cofix f = val_tuple ~name:"pcofixpoint"[|val_int;val_prec f|]
 
 type cast_kind = VMcast | DEFAULTcast
 let val_cast = val_enum "cast_kind" 2
@@ -262,7 +261,7 @@ let rec exliftn el c = match c with
 (* Lifting the binding depth across k bindings *)
 
 let liftn k n =
-  match el_liftn (pred n) (el_shft k ELID) with
+  match el_liftn (pred n) (el_shft k el_id) with
     | ELID -> (fun c -> c)
     | el -> exliftn el
 
@@ -313,22 +312,15 @@ let subst1 lam = substl [lam]
 (***************************************************************************)
 
 let val_ndecl =
-  val_tuple"named_declaration"[|val_id;val_opt val_constr;val_constr|]
+  val_tuple ~name:"named_declaration"[|val_id;val_opt val_constr;val_constr|]
 let val_rdecl =
-  val_tuple"rel_declaration"[|val_name;val_opt val_constr;val_constr|]
+  val_tuple ~name:"rel_declaration"[|val_name;val_opt val_constr;val_constr|]
 let val_nctxt = val_list val_ndecl
 let val_rctxt = val_list val_rdecl
 
 type named_declaration = identifier * constr option * constr
 type rel_declaration = name * constr option * constr
 
-let map_named_declaration f (id, v, ty) = (id, Option.map f v, f ty)
-let map_rel_declaration = map_named_declaration
-
-let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a)
-let fold_rel_declaration = fold_named_declaration
-
-
 type named_context = named_declaration list
 let empty_named_context = []
 let fold_named_context f l ~init = List.fold_right f l init
@@ -439,7 +431,6 @@ let decompose_prod_n_assum n =
 (***************************)
 
 type arity = rel_context * sorts
-let val_arity = val_tuple"arity"[|val_rctxt;val_constr|]
 
 let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign
 
-- 
cgit v1.2.3