Imported Upstream version 8.0pl2upstream/8.0pl2

12 files changed, 137 insertions, 137 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 2126f015..378eee30 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml,v 1.111.2.1 2004/07/16 19:30:43 herbelin Exp $ *)
+(* $Id: cases.ml,v 1.111.2.4 2004/12/09 20:07:01 herbelin Exp $ *)
 
 open Util
 open Names
@@ -262,9 +262,10 @@ type tomatch_stack = tomatch_status list
 
 (* The type [predicate_signature] types the terms to match and the rhs:
 
-   - [PrLetIn (n,dep,pred)] types a pushed term ([Pushed]), if dep is true,
-     the term is dependent, if n<>0 then the type of the pushed term is
-     necessarily inductive with n real arguments. Otherwise, it may be
+   - [PrLetIn (names,dep,pred)] types a pushed term ([Pushed]), 
+     if dep<>Anonymous, the term is dependent, let n=|names|, if 
+     n<>0 then the type of the pushed term is necessarily an
+     inductive with n real arguments. Otherwise, it may be
      non inductive, or inductive without real arguments, or inductive
      originating from a subterm in which case real args are not dependent;
      it accounts for n+1 binders if dep or n binders if not dep
@@ -274,7 +275,7 @@ type tomatch_stack = tomatch_status list
 *)
 
 type predicate_signature =
-  | PrLetIn of (int * bool) * predicate_signature
+  | PrLetIn of (name list * name) * predicate_signature
   | PrProd of predicate_signature
   | PrCcl of constr
 
@@ -408,12 +409,11 @@ let inh_coerce_to_ind isevars env tmloc ty tyi =
   let hole_source = match tmloc with 
     | Some loc -> fun i -> (loc, TomatchTypeParameter (tyi,i))
     | None -> fun _ -> (dummy_loc, InternalHole) in
-   let (_,evarl,_) =
+   let (evarl,_) =
     List.fold_right
-      (fun (na,ty) (env,evl,n) ->
-	 (push_rel (na,None,ty) env,
-	    (new_isevar isevars env (hole_source n) ty)::evl,n+1))
-      ntys (env,[],1) in
+      (fun (na,ty) (evl,n) ->
+	(new_isevar isevars env (hole_source n) (substl evl ty))::evl,n+1)
+      ntys ([],1) in
   let expected_typ = applist (mkInd tyi,evarl) in
      (* devrait être indifférent d'exiger leq ou pas puisque pour 
         un inductif cela doit être égal *)
@@ -976,10 +976,17 @@ let rec map_predicate f k = function
   | PrCcl ccl -> PrCcl (f k ccl)
   | PrProd pred ->
       PrProd (map_predicate f (k+1) pred)
-  | PrLetIn ((nargs,dep as tm),pred) ->
-      let k' = nargs + (if dep then 1 else 0) in
+  | PrLetIn ((names,dep as tm),pred) ->
+      let k' = List.length names + (if dep<>Anonymous then 1 else 0) in
       PrLetIn (tm, map_predicate f (k+k') pred)
 
+let rec noccurn_predicate k = function
+  | PrCcl ccl -> noccurn k ccl
+  | PrProd pred -> noccurn_predicate (k+1) pred
+  | PrLetIn ((names,dep as tm),pred) ->
+      let k' = List.length names + (if dep<>Anonymous then 1 else 0) in
+      noccurn_predicate (k+k') pred
+
 let liftn_predicate n = map_predicate (liftn n)
 
 let lift_predicate n = liftn_predicate n 1
@@ -998,12 +1005,12 @@ let subst_predicate (args,copt) pred =
 let specialize_predicate_var (cur,typ) = function
   | PrProd _ | PrCcl _ ->
      anomaly "specialize_predicate_var: a pattern-variable must be pushed"
-  | PrLetIn ((0,dep),pred) ->
-      subst_predicate ([],if dep then Some cur else None) pred
+  | PrLetIn (([],dep),pred) ->
+      subst_predicate ([],if dep<>Anonymous then Some cur else None) pred
   | PrLetIn ((_,dep),pred) ->
       (match typ with
         | IsInd (_,IndType (_,realargs)) ->
-            subst_predicate (realargs,if dep then Some cur else None) pred
+           subst_predicate (realargs,if dep<>Anonymous then Some cur else None) pred
         | _ -> anomaly "specialize_predicate_var")
 
 let ungeneralize_predicate = function
@@ -1020,9 +1027,9 @@ let ungeneralize_predicate = function
 (* then we have to replace x by x' in t(x) and y by y' in P                  *)
 (*****************************************************************************)
 let generalize_predicate c ny d = function
-  | PrLetIn ((nargs,dep as tm),pred) ->
-      if not dep then anomaly "Undetected dependency";
-      let p = nargs + 1 in
+  | PrLetIn ((names,dep as tm),pred) ->
+      if dep=Anonymous then anomaly "Undetected dependency";
+      let p = List.length names + 1 in
       let pred = lift_predicate 1 pred in
       let pred = regeneralize_index_predicate (ny+p+1) pred in
       PrLetIn (tm, PrProd pred)
@@ -1038,18 +1045,18 @@ let rec extract_predicate l = function
   | PrProd pred, Abstract d'::tms ->
       let d' = map_rel_declaration (lift (List.length l)) d' in
       substl l (mkProd_or_LetIn d' (extract_predicate [] (pred,tms)))
-  | PrLetIn ((0,dep),pred), Pushed ((cur,_),_)::tms ->
-      extract_predicate (if dep then cur::l else l) (pred,tms)
+  | PrLetIn (([],dep),pred), Pushed ((cur,_),_)::tms ->
+      extract_predicate (if dep<>Anonymous then cur::l else l) (pred,tms)
   | PrLetIn ((_,dep),pred), Pushed ((cur,IsInd (_,(IndType(_,realargs)))),_)::tms ->
       let l = List.rev realargs@l in
-      extract_predicate (if dep then cur::l else l) (pred,tms)
+      extract_predicate (if dep<>Anonymous then cur::l else l) (pred,tms)
   | PrCcl ccl, [] ->
       substl l ccl
   | _ -> anomaly"extract_predicate: predicate inconsistent with terms to match"
 
 let abstract_predicate env sigma indf cur tms = function
   | (PrProd _ | PrCcl _) -> anomaly "abstract_predicate: must be some LetIn"
-  | PrLetIn ((nrealargs,dep),pred) ->
+  | PrLetIn ((names,dep),pred) ->
       let sign = make_arity_signature env true indf in
       (* n is the number of real args + 1 *)
       let n = List.length sign in
@@ -1061,18 +1068,24 @@ let abstract_predicate env sigma indf cur tms = function
       (* Depending on whether the predicate is dependent or not, and has real
          args or not, we lift it to make room for [sign] *)
       (* Even if not intrinsically dep, we move the predicate into a dep one *)
-      let k =
-        if nrealargs = 0 & n <> 1 then 
-          (* Real args were not considered *) if dep then n-1 else n
+      let sign,k =
+        if names = [] & n <> 1 then 
+          (* Real args were not considered *) 
+          (if dep<>Anonymous then
+            ((let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign),n-1)
+          else
+            (sign,n))
         else
-          (* Real args are OK *) if dep then 0 else 1 in
+          (* Real args are OK *)
+          (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign,
+           if dep<>Anonymous then 0 else 1) in
       let pred = lift_predicate k pred in
       let pred = extract_predicate [] (pred,tms) in
       (true, it_mkLambda_or_LetIn_name env pred sign)
 
 let rec known_dependent = function
   | None -> false
-  | Some (PrLetIn ((_,dep),_)) -> dep
+  | Some (PrLetIn ((_,dep),_)) -> dep<>Anonymous
   | Some (PrCcl _) -> false
   | Some (PrProd _) ->
       anomaly "known_dependent: can only be used when patterns remain"
@@ -1084,10 +1097,13 @@ let rec known_dependent = function
 
 let expand_arg n alreadydep (na,t) deps (k,pred) =
   (* current can occur in pred even if the original problem is not dependent *)
-  let dep = deps <> [] || alreadydep in
-  let pred = if dep then pred else lift_predicate (-1) pred in
+  let dep =
+    if alreadydep<>Anonymous then alreadydep
+    else if deps = [] && noccurn_predicate 1 pred then Anonymous
+    else Name (id_of_string "x") in
+  let pred = if dep<>Anonymous then pred else lift_predicate (-1) pred in
   (* There is no dependency in realargs for subpattern *)
-  (k-1, PrLetIn ((0,dep), pred))
+  (k-1, PrLetIn (([],dep), pred))
 
 
 (*****************************************************************************)
@@ -1107,14 +1123,15 @@ let expand_arg n alreadydep (na,t) deps (k,pred) =
 let specialize_predicate tomatchs deps cs = function
   | (PrProd _ | PrCcl _) ->
       anomaly "specialize_predicate: a matched pattern must be pushed"
-  | PrLetIn ((nrealargs,isdep),pred) ->
+  | PrLetIn ((names,isdep),pred) ->
       (* Assume some gamma st: gamma, (X,x:=realargs,copt) |- pred *)
-      let k = nrealargs + (if isdep then 1 else 0) in
+      let nrealargs = List.length names in
+      let k = nrealargs + (if isdep<>Anonymous then 1 else 0) in
       (* We adjust pred st: gamma, x1..xn, (X,x:=realargs,copt) |- pred' *)
       let n = cs.cs_nargs in
       let pred' = liftn_predicate n (k+1) pred in
       let argsi = if nrealargs <> 0 then Array.to_list cs.cs_concl_realargs else [] in
-      let copti = if isdep then Some (build_dependent_constructor cs) else None in
+      let copti = if isdep<>Anonymous then Some (build_dependent_constructor cs) else None in
       (* The substituends argsi, copti are all defined in gamma, x1...xn *)
       (* We need _parallel_ bindings to get gamma, x1...xn |- pred'' *)
       let pred'' = subst_predicate (argsi, copti) pred' in
@@ -1513,24 +1530,28 @@ let extract_predicate_conclusion isdep tomatchl pred =
   let cook = function
     | _,IsInd (_,IndType(_,args)) -> Some (List.length args)
     | _,NotInd _ -> None in
-  let decomp_lam_force p =
+  let rec decomp_lam_force n l p =
+    if n=0 then (l,p) else
     match kind_of_term p with
-      | Lambda (_,_,c) -> c
-      | _ -> (* eta-expansion *) applist (lift 1 p, [mkRel 1]) in
-  let rec buildrec p = function
-    | [] -> p
+      | Lambda (na,_,c) -> decomp_lam_force (n-1) (na::l) c
+      | _ -> (* eta-expansion *) 
+          let na = Name (id_of_string "x") in
+          decomp_lam_force (n-1) (na::l) (applist (lift 1 p, [mkRel 1])) in
+  let rec buildrec allnames p = function
+    | [] -> (List.rev allnames,p)
     | tm::ltm ->
 	match cook tm with
 	  | None -> 
               let p = 
                 (* adjust to a sign containing the NotInd's *)
                 if isdep then lift 1 p else p in
-              buildrec p ltm 
+              let names = if isdep then [Anonymous] else [] in
+              buildrec (names::allnames) p ltm 
 	  | Some n ->
               let n = if isdep then n+1 else n in
-              let p = iterate decomp_lam_force n p in
-              buildrec p ltm
-  in buildrec pred tomatchl
+              let names,p = decomp_lam_force n [] p in
+              buildrec (names::allnames) p ltm
+  in buildrec [] pred tomatchl
 
 let set_arity_signature dep n arsign tomatchl pred x =
   (* avoid is not exhaustive ! *)
@@ -1572,18 +1593,19 @@ let set_arity_signature dep n arsign tomatchl pred x =
   decomp_block [] pred (tomatchl,arsign)
 
 let prepare_predicate_from_tycon loc dep env isevars tomatchs c =
-  let cook (n, l, env) = function
+  let cook (n, l, signs) = function
     | c,IsInd (_,IndType(indf,realargs)) ->
 	let indf' = lift_inductive_family n indf in
-	let sign = make_arity_signature env dep indf' in
+	let arsign = make_arity_signature env dep indf' in
 	let p = List.length realargs in
 	if dep then
-	  (n + p + 1, c::(List.rev realargs)@l, push_rels sign env)
+	  (n + p + 1, c::(List.rev realargs)@l, arsign::signs)
 	else
-	  (n + p, (List.rev realargs)@l, push_rels sign env)
+	  (n + p, (List.rev realargs)@l, arsign::signs)
     | c,NotInd _ ->
-	(n, l, env) in
-  let n, allargs, env = List.fold_left cook (0, [], env) tomatchs in
+	(n, l, []::signs) in
+  let n, allargs, signs = List.fold_left cook (0, [], []) tomatchs in
+  let env = List.fold_right push_rels signs env in
   let allargs =
     List.map (fun c -> lift n (nf_betadeltaiota env (evars_of isevars) c)) allargs in
   let rec build_skeleton env c =
@@ -1594,28 +1616,32 @@ let prepare_predicate_from_tycon loc dep env isevars tomatchs c =
       mkExistential isevars env (loc, CasesType)
     else
       map_constr_with_full_binders push_rel build_skeleton env c in
-  build_skeleton env (lift n c)
+ List.rev (List.map (List.map pi1) signs), build_skeleton env (lift n c)
   
 (* Here, [pred] is assumed to be in the context built from all *)
 (* realargs and terms to match *)
-let build_initial_predicate isdep pred tomatchl =
-  let nar = List.fold_left (fun n (_,t) ->
-    let p = match t with IsInd (_,IndType(_,a)) -> List.length a | _ -> 0 in
-    if isdep then n+p+1 else n+p) 0 tomatchl in
-  let cook = function
-    | _,IsInd (_,IndType(_,realargs)) -> List.length realargs
-    | _,NotInd _ -> 0 in
+let build_initial_predicate isdep allnames pred =
+  let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
   let rec buildrec n pred = function
     | [] -> PrCcl pred
-    | tm::ltm ->
-        let nrealargs = cook tm in
+    | names::lnames ->
+        let names' = if isdep then List.tl names else names in
+        let n' = n + List.length names' in
         let pred, p, user_p =
           if isdep then 
-            if dependent (mkRel (nar-n)) pred then pred, 1, 1
-            else liftn (-1) (nar-n) pred, 0, 1
+            if dependent (mkRel (nar-n')) pred then pred, 1, 1
+            else liftn (-1) (nar-n') pred, 0, 1
           else pred, 0, 0 in
-	PrLetIn ((nrealargs,p=1), buildrec (n+nrealargs+user_p) pred ltm)
-  in buildrec 0 pred tomatchl
+        let na = 
+          if p=1 then
+            let na = List.hd names in
+            if na = Anonymous then
+              (* peut arriver en raison des evars *)
+              Name (id_of_string "x") (*Hum*)
+            else na
+          else Anonymous in
+	PrLetIn ((names',na), buildrec (n'+user_p) pred lnames)
+  in buildrec 0 pred allnames
 
 let extract_arity_signature env0 tomatchl tmsign =
   let get_one_sign n tm {contents = (na,t)} =
@@ -1652,9 +1678,9 @@ let extract_arity_signature env0 tomatchl tmsign =
     | [],[] -> []
     | (_,tm)::ltm, x::tmsign ->
 	let l = get_one_sign n tm x in
-	(buildrec (n + List.length l) (ltm,tmsign)) @ l
+	l :: buildrec (n + List.length l) (ltm,tmsign)
     | _ -> assert false
-  in buildrec 0 (tomatchl,tmsign)
+  in List.rev (buildrec 0 (tomatchl,tmsign))
 
 (* Builds the predicate. If the predicate is dependent, its context is
  * made of 1+nrealargs assumptions for each matched term in an inductive
@@ -1683,17 +1709,18 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
       (match tycon with
        | None -> None
        | Some t ->
-	 let pred = prepare_predicate_from_tycon loc false env isevars tomatchs t in
-	 Some (build_initial_predicate false pred tomatchs))
+	 let names,pred = prepare_predicate_from_tycon loc false env isevars tomatchs t in
+	 Some (build_initial_predicate false names pred))
 
   (* v8 style type annotation *)
   | (None,{contents = Some rtntyp}) ->
 
       (* We extract the signature of the arity *)
-      let arsign = extract_arity_signature env tomatchs sign in
-      let env = push_rels arsign env in
+      let arsigns = extract_arity_signature env tomatchs sign in
+      let env = List.fold_right push_rels arsigns env in
+      let allnames = List.rev (List.map (List.map pi1) arsigns) in
       let predccl = (typing_fun (mk_tycon (new_Type ())) env rtntyp).uj_val in
-      Some (build_initial_predicate true predccl tomatchs)
+      Some (build_initial_predicate true allnames predccl)
 
   (* v7 style type annotation; set the v8 annotation by side effect *)
   | (Some pred,x) ->
@@ -1721,12 +1748,9 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
 	error_wrong_predicate_arity_loc
 	  loc env predj.uj_val ndep_arity dep_arity
       in
-      let predccl = extract_predicate_conclusion dep tomatchs predj.uj_val in
-(*
-      let etapred,cdep = case_dependent env (evars_of isevars) loc predj tomatchs in
-*)
+      let ln,predccl= extract_predicate_conclusion dep tomatchs predj.uj_val in
       set_arity_signature dep n sign tomatchs pred x;
-      Some (build_initial_predicate dep predccl tomatchs)
+      Some (build_initial_predicate dep ln predccl)
 
 
 (**************************************************************************)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6f396b43..0ee95a0f 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarconv.ml,v 1.44.6.1 2004/07/16 19:30:44 herbelin Exp $ *)
+(* $Id: evarconv.ml,v 1.44.6.2 2004/11/26 23:51:39 herbelin Exp $ *)
 
 open Util
 open Names
@@ -39,8 +39,11 @@ let flex_kind_of_term c l =
 let eval_flexible_term env c =
   match kind_of_term c with
   | Const c -> constant_opt_value env c
-  | Rel n -> let (_,v,_) = lookup_rel n env in option_app (lift n) v
-  | Var id -> let (_,v,_) = lookup_named id env in v
+  | Rel n ->
+      (try let (_,v,_) = lookup_rel n env in option_app (lift n) v
+      with Not_found -> None)
+  | Var id ->
+      (try let (_,v,_) = lookup_named id env in v with Not_found -> None)
   | LetIn (_,b,_,c) -> Some (subst1 b c)
   | Lambda _ -> Some c
   | _ -> assert false
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 441070fe..4337c0fc 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarutil.ml,v 1.64.2.3 2004/07/16 19:30:44 herbelin Exp $ *)
+(* $Id: evarutil.ml,v 1.64.2.5 2004/12/09 14:45:38 herbelin Exp $ *)
 
 open Util
 open Pp
@@ -30,25 +30,6 @@ let rec filter_unique = function
       if List.mem x l then filter_unique (List.filter (fun y -> x<>y) l)
       else x::filter_unique l
 
-(*
-let distinct_id_list = 
-  let rec drec fresh = function
-      [] -> List.rev fresh 
-    | id::rest ->
- 	let id' = next_ident_away_from id fresh in drec (id'::fresh) rest
-  in drec []
-*)
-
-(*
-let filter_sign p sign x =
-  sign_it
-    (fun id ty (v,ids,sgn) ->
-      let (disc,v') = p v (id,ty) in
-      if disc then (v', id::ids, sgn) else (v', ids, add_sign (id,ty) sgn))
-    sign
-    (x,[],nil_sign)
-*)
-
 (* Expanding existential variables (pretyping.ml) *)
 (* 1- whd_ise fails if an existential is undefined *)
 
@@ -183,20 +164,9 @@ let do_restrict_hyps sigma ev args =
   let evd = Evd.map sigma ev in
   let env = evar_env evd in
   let hyps = evd.evar_hyps in
-  let (_,(rsign,ncargs)) =
-    List.fold_left 
-      (fun (sign,(rs,na)) a ->
-	 (List.tl sign,
-	  if not(closed0 a) then 
-	    (rs,na)
-	  else 
-	    (add_named_decl (List.hd sign) rs, a::na)))
-      (hyps,([],[])) args 
-  in
-  let sign' = List.rev rsign in
-  let env' = reset_with_named_context sign' env in
-  let instance = make_evar_instance env' in
-  let (sigma',nc) = new_isevar_sign env' sigma evd.evar_concl instance in
+  let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in
+  let env' = reset_with_named_context sign env in
+  let (sigma',nc) = new_isevar_sign env' sigma evd.evar_concl ncargs in
   let nc = refresh_universes nc in (* needed only if nc is an inferred type *)
   let sigma'' = Evd.define sigma' ev nc in
   (sigma'', nc)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 24a8fbc7..c33a261b 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductiveops.ml,v 1.14.2.1 2004/07/16 19:30:45 herbelin Exp $ *)
+(* $Id: inductiveops.ml,v 1.14.2.2 2004/12/29 12:15:00 herbelin Exp $ *)
 
 open Util
 open Names
@@ -341,9 +341,9 @@ let control_only_guard env =
 	Inductive.check_fix env fix; 
 	Array.iter control_rec tys;
 	Array.iter control_rec bds;
-    | Case(_,p,c,b) ->control_rec p;control_rec c;Array.iter control_rec b
+    | Case(_,p,c,b) -> control_rec p;control_rec c;Array.iter control_rec b
     | Evar (_,cl)         -> Array.iter control_rec cl
-    | App (_,cl)         -> Array.iter control_rec cl
+    | App (c,cl)         -> control_rec c; Array.iter control_rec cl
     | Cast (c1,c2)       -> control_rec c1; control_rec c2
     | Prod (_,c1,c2)     -> control_rec c1; control_rec c2
     | Lambda (_,c1,c2)   -> control_rec c1; control_rec c2
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index a8dcef29..8cfa9b3c 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductiveops.mli,v 1.10.2.1 2004/07/16 19:30:45 herbelin Exp $ *)
+(*i $Id: inductiveops.mli,v 1.10.2.3 2005/01/21 17:19:37 herbelin Exp $ i*)
 
 open Names
 open Term
@@ -66,7 +66,7 @@ val make_arity_signature :
 val make_arity : env -> bool -> inductive_family -> sorts -> types
 val build_branch_type : env -> bool -> constr -> constructor_summary -> types
 
-(* Raise Not_found if not given an valid inductive type *)
+(* Raise [Not_found] if not given an valid inductive type *)
 val extract_mrectype : constr -> inductive * constr list
 val find_mrectype    : env -> evar_map -> constr -> inductive * constr list
 val find_rectype     : env -> evar_map -> constr -> inductive_type
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 808c46a4..2f666880 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: matching.mli,v 1.3.2.1 2004/07/16 19:30:45 herbelin Exp $ i*)
+(*i $Id: matching.mli,v 1.3.2.2 2005/01/21 16:42:37 herbelin Exp $ i*)
 
 (*i*)
 open Names
@@ -42,7 +42,7 @@ val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
 (* To skip to the next occurrence *)
 exception NextOccurrence of int
 
-(* Tries to match a _closed_ subterm of [c] with [pat] *)
+(* Tries to match a **closed** subterm of [c] with [pat] *)
 val sub_match : int -> constr_pattern -> constr -> patvar_map * constr
 
 (* [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 80ab1b6e..f58a12c6 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pattern.ml,v 1.24.2.1 2004/07/16 19:30:45 herbelin Exp $ *)
+(* $Id: pattern.ml,v 1.24.2.2 2004/11/26 17:51:52 herbelin Exp $ *)
 
 open Util
 open Names
@@ -182,8 +182,7 @@ let rec pattern_of_constr t =
 	       Some (pattern_of_constr p),pattern_of_constr a,
 	       Array.map pattern_of_constr br)
     | Fix f -> PFix f
-    | CoFix _ ->
-	error "pattern_of_constr: (co)fix currently not supported"
+    | CoFix f -> PCoFix f
 
 (* To process patterns, we need a translation without typing at all. *)
 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 520f09e9..ef4a4670 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: rawterm.ml,v 1.43.2.2 2004/07/16 19:30:46 herbelin Exp $ *)
+(* $Id: rawterm.ml,v 1.43.2.4 2004/12/29 10:17:10 herbelin Exp $ *)
 
 (*i*)
 open Util
@@ -49,7 +49,7 @@ type 'a bindings =
 type 'a with_bindings = 'a * 'a bindings
 
 type hole_kind =
-  | ImplicitArg of global_reference * int
+  | ImplicitArg of global_reference * (int * identifier option)
   | BinderType of name
   | QuestionMark
   | CasesType
@@ -356,7 +356,7 @@ type ('a,'b) red_expr_gen =
   | Unfold of 'b occurrences list
   | Fold of 'a list
   | Pattern of 'a occurrences list
-  | ExtraRedExpr of string * 'a
+  | ExtraRedExpr of string
 
 type ('a,'b) may_eval =
   | ConstrTerm of 'a
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index d78d1866..97e11af6 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: rawterm.mli,v 1.47.2.2 2004/07/16 19:30:46 herbelin Exp $ i*)
+(*i $Id: rawterm.mli,v 1.47.2.5 2005/01/21 16:42:37 herbelin Exp $ i*)
 
 (*i*)
 open Util
@@ -47,7 +47,7 @@ type 'a bindings =
 type 'a with_bindings = 'a * 'a bindings
 
 type hole_kind =
-  | ImplicitArg of global_reference * int
+  | ImplicitArg of global_reference * (int * identifier option)
   | BinderType of name
   | QuestionMark
   | CasesType
@@ -97,11 +97,11 @@ i*)
 
 val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr
 
-(*
+(*i
 val map_rawconstr_with_binders_loc : loc -> 
   (identifier -> 'a -> identifier * 'a) ->
   ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr
-*)
+i*)
 
 val occur_rawconstr : identifier -> rawconstr -> bool
 
@@ -130,7 +130,7 @@ type ('a,'b) red_expr_gen =
   | Unfold of 'b occurrences list
   | Fold of 'a list
   | Pattern of 'a occurrences list
-  | ExtraRedExpr of string * 'a
+  | ExtraRedExpr of string
 
 type ('a,'b) may_eval =
   | ConstrTerm of 'a
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 7e79a4fe..f225e79f 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacred.ml,v 1.75.2.2 2004/07/16 19:30:46 herbelin Exp $ *)
+(* $Id: tacred.ml,v 1.75.2.6 2004/12/29 10:17:10 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -329,7 +329,7 @@ let make_elim_fun (names,(nbfix,lv,n)) largs =
 	   mkLambda (Name(id_of_string"x"),
 		     substl (rev_firstn_liftn (n-k) (-i) la') a,
 		     c))
-	0 (applistc (mkEvalRef ref) la') lv)
+	1 (applistc (mkEvalRef ref) la') (List.rev lv))
 
 (* [f] is convertible to [Fix(recindices,bodynum),bodyvect)] make 
    the reduction using this extra information *)
@@ -808,6 +808,7 @@ let abstract_scheme env sigma (locc,a) t =
 
 let pattern_occs loccs_trm env sigma c =
   let abstr_trm = List.fold_right (abstract_scheme env sigma) loccs_trm c in
+  let _ = Typing.type_of env sigma abstr_trm in
   applist(abstr_trm, List.map snd loccs_trm)
 
 (* Generic reduction: reduction functions used in reduction tactics *)
@@ -858,7 +859,7 @@ let reduction_of_redexp = function
   | Unfold ubinds -> unfoldn ubinds
   | Fold cl -> fold_commands cl
   | Pattern lp -> pattern_occs lp
-  | ExtraRedExpr (s,c) ->
+  | ExtraRedExpr s ->
       (try Stringmap.find s !red_expr_tab
       with Not_found -> error("unknown user-defined reduction \""^s^"\""))
 (* Used in several tactics. *)
@@ -945,7 +946,10 @@ let reduce_to_ref_gen allow_product env sigma ref t =
           try 
 	    let t' = nf_betaiota (one_step_reduce env sigma t) in 
 	    elimrec env t' l
-          with NotStepReducible -> raise Not_found
+          with NotStepReducible -> 
+	    errorlabstrm ""
+	    (str "Not a statement of conclusion " ++ 
+	     Nametab.pr_global_env Idset.empty ref)
   in
   elimrec env t []
 
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 162275d5..7998a8fd 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacred.mli,v 1.21.2.1 2004/07/16 19:30:46 herbelin Exp $ i*)
+(*i $Id: tacred.mli,v 1.21.2.2 2005/01/21 16:42:37 herbelin Exp $ i*)
 
 (*i*)
 open Names
@@ -62,7 +62,7 @@ val reduce_to_atomic_ind : env ->  evar_map -> types -> inductive * types
 val reduce_to_quantified_ind : env ->  evar_map -> types -> inductive * types
 
 (* [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form
-   [t'=(x1:A1)..(xn:An)(ref args)] and raise Not_found if not possible *)
+   [t'=(x1:A1)..(xn:An)(ref args)] and raise [Not_found] if not possible *)
 val reduce_to_quantified_ref :
   env ->  evar_map -> Libnames.global_reference -> types -> types
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index dd9742ea..22bd0aba 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: termops.mli,v 1.21.2.1 2004/07/16 19:30:46 herbelin Exp $ *)
+(*i $Id: termops.mli,v 1.21.2.3 2005/01/21 17:19:37 herbelin Exp $ i*)
 
 open Util
 open Pp
@@ -16,7 +16,7 @@ open Sign
 open Environ
 
 (* Universes *)
-(*val set_module : Names.dir_path -> unit*)
+(*i val set_module : Names.dir_path -> unit i*)
 val new_univ : unit -> Univ.universe
 val new_sort_in_family : sorts_family -> sorts