Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 25 insertions, 14 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e8c6073e..b3be7afd 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -1,12 +1,17 @@
 (************************************************************************)
 (*  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: recordops.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* Created by Amokrane Saïbi, Dec 1998 *)
+(* Addition of products and sorts in canonical structures by Pierre
+   Corbineau, Feb 2008 *)
+
+(* This file registers properties of records: projections and
+   canonical structures *)
 
 open Util
 open Pp
@@ -14,7 +19,6 @@ open Names
 open Libnames
 open Nametab
 open Term
-open Termops
 open Typeops
 open Libobject
 open Library
@@ -39,6 +43,12 @@ type struc_typ = {
 let structure_table = ref (Indmap.empty : struc_typ Indmap.t)
 let projection_table = ref Cmap.empty
 
+(* TODO: could be unify struc_typ and struc_tuple ? in particular,
+   is the inductive always (fst constructor) ? It seems so... *)
+
+type struc_tuple =
+    inductive * constructor * (name * bool) list * constant option list
+
 let load_structure i (_,(ind,id,kl,projs)) =
   let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
   let struc =
@@ -71,7 +81,7 @@ let discharge_structure (_,(ind,id,kl,projs)) =
   Some (Lib.discharge_inductive ind, discharge_constructor id, kl,
         List.map (Option.map Lib.discharge_con) projs)
 
-let (inStruc,outStruc) =
+let inStruc : struc_tuple -> obj =
   declare_object {(default_object "STRUCTURE") with
     cache_function = cache_structure;
     load_function = load_structure;
@@ -130,7 +140,7 @@ open Libobject
 let load_method (_,(ty,id)) =
   meth_dnet := MethodsDnet.add ty id !meth_dnet
 
-let (in_method,out_method) =
+let in_method : constr * MethodsDnet.ident -> obj =
   declare_object
     { (default_object "RECMETHODS") with
 	load_function = (fun _ -> load_method);
@@ -201,7 +211,7 @@ let cs_pattern_of_constr t =
 	      _ -> raise Not_found
 	end
     | Rel n -> Default_cs, pred n, []
-    | Prod (_,a,b) when not (dependent (mkRel 1) b) -> Prod_cs, -1, [a;pop b]
+    | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, -1, [a; Termops.pop b]
     | Sort s -> Sort_cs (family_of_sort s), -1, []
     | _ ->
 	begin
@@ -235,7 +245,7 @@ let compute_canonical_projections (con,ind) =
                      (let con_pp = Nametab.pr_global_env Idset.empty (ConstRef con)
                       and proji_sp_pp = Nametab.pr_global_env Idset.empty (ConstRef proji_sp) in
 		      msg_warning (str "No global reference exists for projection value"
-                                   ++ print_constr t ++ str " in instance "  
+                                   ++ Termops.print_constr t ++ str " in instance "  
                                    ++ con_pp ++ str " of " ++ proji_sp_pp ++ str ", ignoring it."));
 		   l
 	       end
@@ -285,7 +295,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) =
 let discharge_canonical_structure (_,(cst,ind)) =
   Some (Lib.discharge_con cst,Lib.discharge_inductive ind)
 
-let (inCanonStruc,outCanonStruct) =
+let inCanonStruc : constant * inductive -> obj =
   declare_object {(default_object "CANONICAL-STRUCTURE") with
     open_function = open_canonical_structure;
     cache_function = cache_canonical_structure;
@@ -323,16 +333,17 @@ let check_and_decompose_canonical_structure ref =
 let declare_canonical_structure ref =
   add_canonical_structure (check_and_decompose_canonical_structure ref)
 
-let outCanonicalStructure x = fst (outCanonStruct x)
-
 let lookup_canonical_conversion (proj,pat) =
   List.assoc pat (Refmap.find proj !object_table)
 
-let is_open_canonical_projection sigma (c,args) =
+let is_open_canonical_projection env sigma (c,args) =
   try
-    let l = Refmap.find (global_of_constr c) !object_table in
-    let n = (snd (List.hd l)).o_NPARAMS in
-    try isEvar_or_Meta (whd_evar sigma (List.nth args n)) with Failure _ -> false
+    let n = find_projection_nparams (global_of_constr c) in
+    try
+      let arg = whd_betadeltaiota env sigma (List.nth args n) in
+      let hd = match kind_of_term arg with App (hd, _) -> hd | _ -> arg in
+      not (isConstruct hd) 
+    with Failure _ -> false
   with Not_found -> false
 
 let freeze () =