More cleaning on Utils and CList. Some parts of the code being

peculiarly messy, I hope I did not introduce too many bugs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15815 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 20 insertions, 12 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 98cc42aaf..b6b8f8dba 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1409,20 +1409,23 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
      - [subst0] is made of items [(p,u,(u,ty))] where [ty] is the type of [u]
        and both are adjusted to [extenv] while [p] is the index of [id] in
        [extenv] (after expansion of the aliases) *)
-  let subst0 = map_succeed (fun (x,u) ->
+  let map (x, u) =
     (* d1 ... dn dn+1 ... dn'-p+1 ... dn' *)
     (* \--env-/          (= x:ty)         *)
     (* \--------------extenv------------/ *)
-    let (p,_,_) = lookup_rel_id x (rel_context extenv) in
+    let (p, _, _) = lookup_rel_id x (rel_context extenv) in
     let rec traverse_local_defs p =
       match pi2 (lookup_rel p extenv) with
       | Some c -> assert (isRel c); traverse_local_defs (p + destRel c)
       | None -> p in
     let p = traverse_local_defs p in
-    let u = lift (n'-n) u in
-    (p,u,expand_vars_in_term extenv u)) subst in
-  let t0 = lift (n'-n) t in
-  (subst0,t0)
+    let u = lift (n' - n) u in
+    try Some (p, u, expand_vars_in_term extenv u)
+      (* pedrot: does this really happen to raise [Failure _]? *)
+    with Failure _ -> None in
+  let subst0 = List.map_filter map subst in
+  let t0 = lift (n' - n) t in
+  (subst0, t0)
 
 let push_binder d (k,env,subst) =
   (k+1,push_rel d env,List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index da5ccc96b..ce84e6bd5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -687,7 +687,8 @@ let simple_cases_matrix_of_branches ind brs =
       let nal,c = it_destRLambda_or_LetIn_names n b in
       let mkPatVar na = PatVar (Loc.ghost,na) in
       let p = PatCstr (Loc.ghost,(ind,i+1),List.map mkPatVar nal,Anonymous) in
-      let ids = map_succeed Nameops.out_name nal in
+      let map name = try Some (Nameops.out_name name) with Failure _ -> None in
+      let ids = List.map_filter map nal in
       (Loc.ghost,ids,[p],c))
     brs
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 9db16baac..f8cd3609a 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -217,12 +217,13 @@ let push_named_rec_types (lna,typarray,_) env =
     (fun e assum -> push_named assum e) env ctxt
 
 let lookup_rel_id id sign =
-  let rec lookrec = function
-    | (n, (Anonymous,_,_)::l) -> lookrec (n+1,l)
-    | (n, (Name id',b,t)::l)  -> if id' = id then (n,b,t) else lookrec (n+1,l)
-    | (_, [])                 -> raise Not_found
+  let rec lookrec n = function
+    | []                     -> raise Not_found
+    | (Anonymous, _, _) :: l -> lookrec (n + 1) l
+    | (Name id', b, t) :: l  ->
+      if Names.id_ord id' id = 0 then (n, b, t) else lookrec (n + 1) l
   in
-  lookrec (1,sign)
+  lookrec 1 sign
 
 (* Constructs either [forall x:t, c] or [let x:=b:t in c] *)
 let mkProd_or_LetIn (na,body,t) c =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index b3e00ebaa..b6bb43868 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -40,7 +40,10 @@ val print_env : env -> std_ppcmds
 val push_rel_assum : name * types -> env -> env
 val push_rels_assum : (name * types) list -> env -> env
 val push_named_rec_types : name array * types array * 'a -> env -> env
+
 val lookup_rel_id : identifier -> rel_context -> int * constr option * types
+(** Associates the contents of an identifier in a [rel_context]. Raise
+    [Not_found] if there is no such identifier. *)
 
 (** builds argument lists matching a block of binders or a context *)
 val rel_vect : int -> int -> constr array