Imported Upstream version 8.3upstream/8.3

3 files changed, 22 insertions, 24 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 9027315e..09603d8b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
+(* $Id: cases.ml 13511 2010-10-06 20:48:16Z herbelin $ *)
 
 open Util
 open Names
@@ -1089,12 +1089,6 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info =
   let names = get_names pb.env cs_args eqns in
   let submat = List.map (fun (tms,eqn) -> prepend_pattern tms eqn) eqns in
   let typs = List.map2 (fun (_,c,t) na -> (na,c,t)) cs_args names in
-  let _,typs',_ =
-    List.fold_right
-      (fun (na,c,t as d) (env,typs,tms) ->
-	 let tms = List.map List.tl tms in
- 	 (push_rel d env, (na,NotInd(c,t))::typs,tms))
-      typs (pb.env,[],List.map fst eqns) in
 
   let dep_sign =
     find_dependencies_signature
@@ -1114,9 +1108,10 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info =
   let pred_is_not_dep =
     noccur_predicate_between 1 (List.length realnames + 1) pb.pred tomatch in
 
-  let typs'' =
+  let typs' =
     list_map2_i
-      (fun i (na,t) deps ->
+      (fun i d deps ->
+        let (na,c,t) = map_rel_declaration (lift i) d in
 	let dep = match dep with
 	  | Name _ as na',k -> (if na <> Anonymous then na else na'),k
 	  | Anonymous,KnownNotDep ->
@@ -1125,15 +1120,13 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info =
 	      else
 		(force_name na,KnownDep)
 	  | _,_ -> anomaly "Inconsistent dependency" in
-	((mkRel i, lift_tomatch_type i t),deps,dep))
-      1 typs' (List.rev dep_sign) in
+	((mkRel i, NotInd (c,t)),deps,dep))
+      1 typs (List.rev dep_sign) in
 
   let pred =
-    specialize_predicate typs'' (realnames,dep) arsign const_info tomatch pb.pred in
-
-  let currents = List.map (fun x -> Pushed x) typs'' in
+    specialize_predicate typs' (realnames,dep) arsign const_info tomatch pb.pred in
 
-  let sign = List.map (fun (na,t) -> mkDeclTomatch na t) typs' in
+  let currents = List.map (fun x -> Pushed x) typs' in
 
   let ind =
     appvect (
@@ -1141,7 +1134,7 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info =
       List.map (lift const_info.cs_nargs) const_info.cs_params),
       const_info.cs_concl_realargs) in
 
-  let cur_alias = lift (List.length sign) current in
+  let cur_alias = lift (List.length typs) current in
   let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in
   let tomatch = List.rev_append currents tomatch in
 
@@ -1150,13 +1143,13 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info =
     raise_pattern_matching_error
       (dummy_loc, pb.env, NonExhaustive (complete_history history));
 
-  sign,
+  typs,
   { pb with
-      env = push_rels sign pb.env;
+      env = push_rels typs pb.env;
       tomatch = tomatch;
       pred = pred;
       history = history;
-      mat = List.map (push_rels_eqn_with_names sign) submat }
+      mat = List.map (push_rels_eqn_with_names typs) submat }
 
 (**********************************************************************
  INVARIANT:
@@ -1597,7 +1590,7 @@ let prepare_predicate_from_arsign_tycon loc tomatchs sign arsign c =
 	  | Rel n when signlen > 1 (* The term is of a dependent type,
 				      maybe some variable in its type appears in the tycon. *) ->
 	      (match tmtype with
-		  NotInd _ -> (* len - signlen, subst*) assert false (* signlen > 1 *)
+		  NotInd _ -> (subst, len - signlen)
 		| IsInd (_, IndType(indf,realargs),_) ->
 		    let subst =
 		      if dependent tm c && List.for_all isRel realargs
@@ -1707,6 +1700,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
     (* We push the initial terms to match and push their alias to rhs' envs *)
     (* names of aliases will be recovered from patterns (hence Anonymous *)
     (* here) *)
+
     let initial_pushed = List.map2 (fun tm na -> Pushed(tm,[],na)) tomatchs nal in
 
     (* A typing function that provides with a canonical term for absurd cases*)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7b4b5e07..1c17ff88 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretyping.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: pretyping.ml 13408 2010-09-11 19:19:04Z herbelin $ *)
 
 open Pp
 open Util
@@ -235,6 +235,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	str " depends on pattern variable name " ++ pr_id id ++
 	str " which is not bound in current context.")
 
+  let protected_get_type_of env sigma c =
+    try Retyping.get_type_of env sigma c
+    with Anomaly _ ->
+      errorlabstrm "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.")
+
   let pretype_id loc env sigma (lvar,unbndltacvars) id =
     try
       let (n,_,typ) = lookup_rel_id id (rel_context env) in
@@ -244,7 +249,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       let (ids,c) = List.assoc id lvar in
       let subst = List.map (invert_ltac_bound_name env id) ids in
       let c = substl subst c in
-      { uj_val = c; uj_type = Retyping.get_type_of env sigma c }
+      { uj_val = c; uj_type = protected_get_type_of env sigma c }
     with Not_found ->
     try
       let (_,_,typ) = lookup_named id env in
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 3d97d8b2..78626854 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -6,14 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: recordops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: recordops.mli 13447 2010-09-21 13:23:45Z letouzey $ i*)
 
 (*i*)
 open Names
 open Nametab
 open Term
 open Libnames
-open Classops
 open Libobject
 open Library
 (*i*)