- Correction de la version simplifiée (filtrage sur deux sig

  imbriqués) du bug 1834, mais le bug 1834 reste ouvert [cases.ml].
- Réactivation de l'interprétation des listes dans "generalize" cassée
  depuis 11072) [tacinterp.ml].
- Bricoles et petit nettoyage en passant [cases.ml et g_vernac.ml4].


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

5 files changed, 82 insertions, 29 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 4089dc03d2..14a40e378b 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -485,6 +485,11 @@ let list_tabulate f len =
   in 
   tabrec 0
 
+let rec list_make n v =
+  if n = 0 then []
+  else if n < 0 then invalid_arg "list_make"
+  else v::list_make (n-1) v
+
 let list_assign l n e = 
   let rec assrec stk = function
     | ((h::t), 0) -> List.rev_append stk (e::t)
@@ -700,6 +705,12 @@ let rec list_filter2 f = function
       if f d l then d::dp', l::lp' else p
   | _ -> invalid_arg "list_filter2"
 
+let rec list_map_filter f = function
+  | [] -> []
+  | x::l ->
+      let l' = list_map_filter f l in
+      match f x with None -> l' | Some y -> y::l'
+
 let list_subset l1 l2 =
   let t2 = Hashtbl.create 151 in
   List.iter (fun x -> Hashtbl.add t2 x ()) l2;
diff --git a/lib/util.mli b/lib/util.mli
index bc1a9cc263..9c0756fc94 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -103,10 +103,12 @@ val list_subtractq : 'a list -> 'a list -> 'a list
 val list_chop : int -> 'a list -> 'a list * 'a list
 (* [list_tabulate f n] builds [[f 0; ...; f (n-1)]] *)
 val list_tabulate : (int -> 'a) -> int -> 'a list
+val list_make : int -> 'a -> 'a list
 val list_assign : 'a list -> int -> 'a -> 'a list
 val list_distinct : 'a list -> bool
 val list_duplicates : 'a list -> 'a list
 val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
+val list_map_filter : ('a -> 'b option) -> 'a list -> 'b list
 (* [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
    [ f ai == ai], then [list_smartmap f l==l] *)
 val list_smartmap : ('a -> 'a) -> 'a list -> 'a list
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 33826c9f18..c128d7ae1e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -377,12 +377,10 @@ GEXTEND Gram
       | IDENT "End"; id = identref -> VernacEndSegment id
 
       (* Requiring an already compiled module *)
-      | IDENT "Require"; export = export_token; specif = specif_token;
-        qidl = LIST1 global ->
-          VernacRequire (export, specif, qidl)
-      | IDENT "Require"; export = export_token; specif = specif_token;
-        filename = ne_string -> 
-	  VernacRequireFrom (export, specif, filename)
+      | IDENT "Require"; export = export_token; qidl = LIST1 global ->
+          VernacRequire (export, None, qidl)
+      | IDENT "Require"; export = export_token; filename = ne_string -> 
+	  VernacRequireFrom (export, None, filename)
       | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
       | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) 
       | IDENT "Include"; expr = module_expr -> VernacInclude(CIME(expr))
@@ -393,11 +391,6 @@ GEXTEND Gram
       | IDENT "Export" -> Some true
       |  -> None ] ]
   ;
-  specif_token:
-    [ [ IDENT "Implementation" -> Some false
-      | IDENT "Specification" -> Some true
-      |  -> None ] ]
-  ;
   of_module_type:
     [ [ ":"; mty = module_type -> (mty, true) 
       | "<:"; mty = module_type -> (mty, false) ] ]
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 9d65e5978c..ff0ccd21a8 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -118,8 +118,8 @@ let mssg_may_need_inversion () =
   str "Found a matching with no clauses on a term unknown to have an empty inductive type"
 
 (* Utils *)
-let make_anonymous_patvars =
-  list_tabulate (fun _ -> PatVar (dummy_loc,Anonymous)) 
+let make_anonymous_patvars n =
+  list_make n (PatVar (dummy_loc,Anonymous)) 
 
 (* Environment management *)
 let push_rels vars env = List.fold_right push_rel vars env
@@ -345,7 +345,7 @@ let try_find_ind env sigma typ realnames =
   let names =
     match realnames with
       | Some names -> names
-      | None -> list_tabulate (fun _ -> Anonymous) (List.length realargs) in
+      | None -> list_make (List.length realargs) Anonymous in
   IsInd (typ,ind,names)
 
 
@@ -548,16 +548,31 @@ let occur_in_rhs na rhs =
     | Anonymous -> false
     | Name id -> List.mem id rhs.rhs_vars
 
-let is_dep_patt eqn = function
+let is_dep_patt_in eqn = function
   | PatVar (_,name) -> occur_in_rhs name eqn.rhs
   | PatCstr _ -> true
 
-let dependencies_in_rhs nargs eqns =
-  if eqns = [] then list_tabulate (fun _ -> false) nargs (* Only "_" patts *)
-  else
-  let deps = List.map (fun (tms,eqn) -> List.map (is_dep_patt eqn) tms) eqns in
-  let columns = matrix_transpose deps in
-  List.map (List.exists ((=) true)) columns
+let mk_dep_patt_row (pats,eqn) =
+  List.map (is_dep_patt_in eqn) pats
+
+let dependencies_in_pure_rhs nargs eqns =
+  if eqns = [] then list_make nargs false (* Only "_" patts *) else
+  let deps_rows = List.map mk_dep_patt_row eqns in
+  let deps_columns = matrix_transpose deps_rows in
+  List.map (List.exists ((=) true)) deps_columns
+
+let dependent_in_decl b d = 
+  fold_rel_declaration (fun c -> (||) (dependent b c)) d false
+
+let rec dep_in_tomatch n = function
+  | (Pushed _ | Alias _) :: l -> dep_in_tomatch n l
+  | Abstract d :: l -> dependent_in_decl (mkRel n) d or dep_in_tomatch (n+1) l
+  | [] -> false
+
+let dependencies_in_rhs nargs current tms eqns =
+  match kind_of_term current with
+  | Rel n when dep_in_tomatch n tms -> list_make nargs true
+  | _ -> dependencies_in_pure_rhs nargs eqns
 
 let dependent_decl a = function
   | (na,None,t) -> dependent a t
@@ -687,7 +702,7 @@ let merge_name get_name obj = function
 let merge_names get_name = List.map2 (merge_name get_name)
 
 let get_names env sign eqns =
-  let names1 = list_tabulate (fun _ -> Anonymous) (List.length sign) in
+  let names1 = list_make (List.length sign) Anonymous in
   (* If any, we prefer names used in pats, from top to bottom *)
   let names2 = 
     List.fold_right
@@ -1091,7 +1106,8 @@ let build_branch current deps (realnames,dep) pb eqns const_info =
 
   let dep_sign =
     find_dependencies_signature
-      (dependencies_in_rhs const_info.cs_nargs eqns) (List.rev typs) in
+      (dependencies_in_rhs const_info.cs_nargs current pb.tomatch eqns) 
+      (List.rev typs) in
 
   (* The dependent term to subst in the types of the remaining UnPushed 
      terms is relative to the current context enriched by topushs *)
@@ -1655,7 +1671,7 @@ let extract_arity_signature env0 tomatchl tmsign =
 		    or nrealargs <> List.length realnal then
 		      anomaly "Ill-formed 'in' clause in cases";
 		  List.rev realnal
-	      | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
+	      | None -> list_make nrealargs Anonymous in
 	  let arsign = fst (get_arity env0 indf') in
 (* 	  let na =  *)
 (* 	    match na with  *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5fb45299f8..20b4abf8a4 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1427,19 +1427,43 @@ let pf_interp_constr ist gl =
 let constr_list_of_VList env = function
   | VList l -> List.map (constr_of_value env) l
   | _ -> raise Not_found
-      
+
+let pf_interp_constr_in_compound_list inj_fun dest_fun interp_fun ist gl l =
+  let env = pf_env gl in
+  let try_expand_ltac_var x =
+    try match dest_fun x with
+    | RVar (_,id), _ ->
+	List.map inj_fun (constr_list_of_VList env (List.assoc id ist.lfun))
+    | _ ->
+	raise Not_found
+    with Not_found ->
+      (*all of dest_fun, List.assoc, constr_list_of_VList may raise Not_found*)
+      [interp_fun ist gl x] in
+  List.flatten (List.map try_expand_ltac_var l)
+
+let pf_interp_constr_list =
+  pf_interp_constr_in_compound_list (fun x -> x) (fun x -> x)
+    (fun ist gl -> interp_constr ist (project gl) (pf_env gl))
+
+(*
 let pf_interp_constr_list_as_list ist gl (c,_ as x) =
   match c with
     | RVar (_,id) ->
         (try constr_list_of_VList (pf_env gl) (List.assoc id ist.lfun)
-        with Not_found -> [interp_constr ist (project gl) (pf_env gl) x])
+        with Not_found -> [])
     | _ -> [interp_constr ist (project gl) (pf_env gl) x]
 
 let pf_interp_constr_list ist gl l =
   List.flatten (List.map (pf_interp_constr_list_as_list ist gl) l)
+*)
 
 let inj_open c = (Evd.empty,c)
 
+let pf_interp_open_constr_list =
+  pf_interp_constr_in_compound_list inj_open (fun x -> x)
+    (fun ist gl -> interp_open_constr None ist (project gl) (pf_env gl))
+
+(*
 let pf_interp_open_constr_list_as_list ist gl (c,_ as x) =
   match c with
     | RVar (_,id) ->
@@ -1452,6 +1476,7 @@ let pf_interp_open_constr_list_as_list ist gl (c,_ as x) =
 
 let pf_interp_open_constr_list ist gl l =
   List.flatten (List.map (pf_interp_open_constr_list_as_list ist gl) l)
+*)
 
 (* Interprets a type expression *)
 let pf_interp_type ist gl =
@@ -1470,6 +1495,14 @@ let interp_pattern ist sigma env (l,c) =
 let pf_interp_constr_with_occurrences ist gl =
   interp_pattern ist (project gl) (pf_env gl)
 
+let pf_interp_constr_with_occurrences_and_name_as_list = 
+  pf_interp_constr_in_compound_list
+    (fun c -> (([],c),Anonymous))
+    (function (([],c),Anonymous) -> c | _ -> raise Not_found)
+    (fun ist gl (occ_c,na) ->
+      (interp_pattern ist (project gl) (pf_env gl) occ_c,
+       interp_fresh_name ist gl na))
+
 let interp_red_expr ist sigma env = function
   | Unfold l -> Unfold (List.map (interp_unfold ist env) l)
   | Fold l -> Fold (List.map (interp_constr ist sigma env) l)
@@ -2080,9 +2113,7 @@ and interp_atomic ist gl = function
 	  (interp_intro_pattern ist gl ipat) c)
   | TacGeneralize cl ->
       h_generalize_gen
-        (List.map (fun (c,na) ->
-	           pf_interp_constr_with_occurrences ist gl c,
-		   interp_fresh_name ist gl na) cl)
+        (pf_interp_constr_with_occurrences_and_name_as_list ist gl cl)
   | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
   | TacLetTac (na,c,clp,b) ->
       let clp = interp_clause ist gl clp in