module Wcclausenv

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

19 files changed, 335 insertions, 98 deletions

diff --git a/Makefile b/Makefile
index 23c155586b..c2197c9944 100644
--- a/Makefile
+++ b/Makefile
@@ -47,16 +47,16 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
 LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \
 	library/global.cmo library/states.cmo library/library.cmo \
 	library/nametab.cmo library/impargs.cmo library/redinfo.cmo \
-        library/declare.cmo
+        library/indrec.cmo library/declare.cmo
 
 PROOFS=proofs/typing_ev.cmo proofs/tacred.cmo \
        proofs/proof_trees.cmo proofs/logic.cmo \
        proofs/refiner.cmo proofs/evar_refiner.cmo \
-       proofs/macros.cmo proofs/tacinterp.cmo # proofs/clenv.cmo
+       proofs/macros.cmo proofs/tacinterp.cmo proofs/clenv.cmo
 
 TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
-        tactics/nbtermdn.cmo tactics/stock.cmo tactics/tacticals.cmo \
-        tactics/pattern.cmo 
+        tactics/nbtermdn.cmo tactics/stock.cmo tactics/pattern.cmo \
+	tactics/wcclausenv.cmo tactics/tacticals.cmo \
 
 PRETYPING=pretyping/astterm.cmo
 
diff --git a/dev/TODO b/dev/TODO
index 8f5fb1ddf9..6b35783a25 100644
--- a/dev/TODO
+++ b/dev/TODO
@@ -1,4 +1,7 @@
 
+ o Declare
+     - declare_eliminations
+
  o Discharge
      - conserver les constantes dans leur section de définition
        et redéfinir des constantes déchargées à la sortie
@@ -32,6 +35,6 @@
      à compléter
 
  o Toplevel
-     - parsing de la ligne de commande : utiliser Arg
+     - parsing de la ligne de commande : utiliser Arg ?
 
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 429d626f1f..0154aa7a96 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -50,6 +50,19 @@ let mis_recargs mis =
 let mis_recarg mis = mis.mis_mip.mind_listrec
 let mis_typename mis = mis.mis_mip.mind_typename
 
+let is_recursive listind = 
+  let rec one_is_rec rvec = 
+    List.exists (function
+		   | Mrec(i)        -> List.mem i listind 
+                   | Imbr(_,_,lvec) -> one_is_rec lvec
+                   | Norec          -> false
+                   | Param(_)       -> false) rvec
+  in 
+  array_exists one_is_rec
+
+let mis_is_recursive mis =
+  is_recursive (interval 0 ((mis_ntypes mis)-1)) (mis_recarg mis)
+
 let mind_nth_type_packet mib n = mib.mind_packets.(n)
 
 (*s Declaration. *)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 46c781eea0..d9a11fe478 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -56,6 +56,7 @@ val mis_kelim : mind_specif -> sorts list
 val mis_recargs : mind_specif -> (recarg list) array array
 val mis_recarg : mind_specif -> (recarg list) array
 val mis_typename : mind_specif -> identifier
+val mis_is_recursive : mind_specif -> bool
 
 val mind_nth_type_packet : 
   mutual_inductive_body -> int -> mutual_inductive_packet
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 93243a4404..1a1ea5bbb4 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -42,7 +42,7 @@ let stack_reduction_of_reduction red_fun env sigma x stack =
   whd_stack env sigma t []
 
 let strong whdfun env sigma = 
-  let rec strongrec = function
+  let rec strongrec t = match whdfun env sigma t with
     | DOP0 _ as t -> t
     (* Cas ad hoc *)
     | DOP1(oper,c) -> DOP1(oper,strongrec c)
@@ -914,8 +914,8 @@ and eqappr cv_pb infos appr1 appr2 =
 
 
 let fconv cv_pb env sigma t1 t2 =
-  let t1 = strong (fun _ -> strip_outer_cast) env sigma t1
-  and t2 = strong (fun _ -> strip_outer_cast) env sigma t2 in
+  let t1 = strong (fun _ _ -> strip_outer_cast) env sigma t1
+  and t2 = strong (fun _ _ -> strip_outer_cast) env sigma t2 in
   if eq_constr t1 t2 then 
     Constraint.empty
   else
@@ -948,8 +948,8 @@ let is_conv_leq env sigma = test_conversion conv_leq env sigma
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
 
-let whd_meta env sigma = function
-  | DOP0(Meta p) as u -> (try List.assoc p (metamap sigma) with Not_found -> u)
+let whd_meta metamap = function
+  | DOP0(Meta p) as u -> (try List.assoc p metamap with Not_found -> u)
   | x -> x
 	
 (* Try to replace all metas. Does not replace metas in the metas' values
@@ -1300,7 +1300,7 @@ let rec whd_ise1 env sigma = function
   | DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ))
   | c -> c
 
-let nf_ise1 env sigma = strong (whd_ise1 env sigma) env sigma
+let nf_ise1 env sigma = strong whd_ise1 env sigma
 
 (* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables
  * Similarly we have is_fmachine1_metas and is_resolve1_metas *)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 585a573449..1ff259e01a 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -177,7 +177,7 @@ val is_conv_leq : unsafe_env -> 'a evar_map -> constr -> constr -> bool
 
 (*s Special-Purpose Reduction Functions *)
 
-val whd_meta : 'a reduction_function
+val whd_meta : (int * constr) list -> constr -> constr
 val plain_instance : (int * constr) list -> constr -> constr
 val instance : (int * constr) list -> 'a reduction_function
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 5113612413..5f8cfefc01 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -172,10 +172,7 @@ val mkMutCaseA : case_info -> constr -> constr -> constr array -> constr
       [typarray = [|t1,...tn|]]
       [funnames = [f1,.....fn]]
       [bodies   = [b1,.....bn]]
-   then 
-
-   [ mkFix recindxs i typarray funnames bodies]
-   
+   then [ mkFix recindxs i typarray funnames bodies]
    constructs the $i$th function of the block  
 
     [Fixpoint f1 [ctx1] = b1
@@ -183,7 +180,7 @@ val mkMutCaseA : case_info -> constr -> constr -> constr array -> constr
      ...
      with     fn [ctxn] = bn.]
 
-   where the lenght of the $j$th context is $ij$.
+   \noindent where the lenght of the $j$th context is $ij$.
 *)
 val mkFix : int array -> int -> typed_type array -> name list 
   -> constr array -> constr
@@ -194,11 +191,8 @@ val mkFixDlam : int array -> int -> typed_type array
 
 (* If [typarray = [|t1,...tn|]]
       [funnames = [f1,.....fn]]
-      [bodies   = [b1,.....bn]]
-   then
-
-      [mkCoFix i typsarray funnames bodies]
-
+      [bodies   = [b1,.....bn]] \par\noindent
+   then [mkCoFix i typsarray funnames bodies]
    constructs the ith function of the block  
    
     [CoFixpoint f1 = b1
diff --git a/lib/pp.mli b/lib/pp.mli
index c4600fcdf0..8906616ac4 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -51,7 +51,7 @@ val tB : 'a ppcmd_token
 val cLOSE : 'a ppcmd_token
 val tCLOSE : 'a ppcmd_token
 
-(*s Pretty-printing functions WITHOUT FLUSH. *)
+(*s Pretty-printing functions \emph{without flush}. *)
 
 val pP_with : Format.formatter -> std_ppcmds -> unit
 val pPNL_with : Format.formatter -> std_ppcmds -> unit
@@ -59,7 +59,7 @@ val warning_with : Format.formatter -> string -> unit
 val wARN_with : Format.formatter -> std_ppcmds -> unit
 val pp_flush_with : Format.formatter -> unit -> unit
 
-(*s Pretty-printing functions WITH FLUSH. *)
+(*s Pretty-printing functions \emph{with flush}. *)
 
 val mSG_with : Format.formatter -> std_ppcmds -> unit
 val mSGNL_with : Format.formatter -> std_ppcmds -> unit
@@ -68,7 +68,7 @@ val mSGNL_with : Format.formatter -> std_ppcmds -> unit
 (*s The following functions are instances of the previous ones on
   [std_ft] and [err_ft]. *)
 
-(*s Pretty-printing functions WITHOUT FLUSH on [stdout] and [stderr]. *)
+(*s Pretty-printing functions \emph{without flush} on [stdout] and [stderr]. *)
 
 val pP : std_ppcmds -> unit
 val pPNL : std_ppcmds -> unit
@@ -80,7 +80,7 @@ val wARN : std_ppcmds -> unit
 val pp_flush : unit -> unit
 val flush_all: unit -> unit
 
-(*s Pretty-printing functions WITH FLUSH on [stdout] and [stderr]. *)
+(*s Pretty-printing functions \emph{with flush} on [stdout] and [stderr]. *)
 
 val mSG : std_ppcmds -> unit
 val mSGNL : std_ppcmds -> unit
diff --git a/lib/util.ml b/lib/util.ml
index f3bc44ebf4..46474ad936 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -320,6 +320,12 @@ let intmap_to_list m = Intmap.fold (fun n v l -> (n,v)::l) m []
 
 let intmap_inv m b = Intmap.fold (fun n v l -> if v = b then n::l else l) m []
 
+let interval n m = 
+  let rec interval_n (l,m) =
+    if n > m then l else interval_n (m::l,pred m)
+  in 
+  interval_n ([],m)
+
 let in_some x = Some x
 
 let out_some = function
diff --git a/lib/util.mli b/lib/util.mli
index 4f992ffd4e..1952dc46cd 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -5,7 +5,10 @@
 open Pp
 (*i*)
 
-(* Errors. [Anomaly] is used for system errors and [UserError] for the
+(* This module contains numerous utility functions on strings, lists,
+   arrays, etc. *)
+
+(*s Errors. [Anomaly] is used for system errors and [UserError] for the
    user's ones. *)
 
 exception Anomaly of string * std_ppcmds
@@ -92,6 +95,8 @@ val intmap_in_dom : int -> 'a Intmap.t -> bool
 val intmap_to_list : 'a Intmap.t -> (int * 'a) list
 val intmap_inv : 'a Intmap.t -> 'a -> int list
 
+val interval : int -> int -> int list
+
 val in_some : 'a -> 'a option
 val out_some : 'a option -> 'a
 val option_app : ('a -> 'b) -> 'a option -> 'b option
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5ec52db76d..21fc10bf73 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -882,8 +882,11 @@ let clenv_type_of ce c =
          | (n,Cltyp typ)    -> (n,typ.rebus))
       (intmap_to_list ce.env)
   in
+  failwith "TODO: clenv_type_of"
+  (***
   (Trad.ise_resolve true (w_Underlying ce.hook) metamap
      (gLOB(w_hyps ce.hook)) c)._TYPE
+  ***)
 
 let clenv_instance_type_of ce c =
   clenv_instance ce (mk_freelisted (clenv_type_of ce c))
@@ -959,7 +962,8 @@ let clenv_typed_fo_resolver clenv gls =
 
 let args_typ gls = 
   let rec decrec l c = match pf_whd_betadeltaiota gls c with
-    | DOP2(Prod,a,DLAM(n,b)) -> decrec ((Environ.named_hd a n,a)::l) b
+    | DOP2(Prod,a,DLAM(n,b)) -> 
+	decrec ((Environ.named_hd Environ.empty_env a n,a)::l) b
     | x -> l
   in 
   decrec []
@@ -984,9 +988,7 @@ let abstract_list_all gls typ c l =
     if pf_conv_x gls (pf_type_of gls p) typ then p else 
       error "abstract_list_all"
   with UserError _ ->
-    let pt = pTERMINENV (gLOB (pf_hyps gls), typ) in
-    errorlabstrm "abstract_list_all"
-      [< 'sTR "cannot find a generalisation of the goal with type : "; pt >]
+    raise (RefinerError (CannotGeneralize (pf_hyps gls,typ)))
 
 let secondOrderAbstraction allow_K gl p oplist clause =
   let (clause',cllist) = 
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index b5675f1a12..de56125af5 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -26,17 +26,16 @@ type 'a clausenv = {
   env : clbinding Intmap.t;
   hook : 'a }
 
-(* templval is the template which we are trying to fill out.
- * templtyp is its type.
- * namenv is a mapping from metavar numbers to names, for
- *        use in instanciating metavars by name.
- * env is the mapping from metavar numbers to their types
- *     and values.
- * hook is the pointer to the current walking context, for
- *      integrating existential vars and metavars.
- *)
+(* [templval] is the template which we are trying to fill out.
+ * [templtyp] is its type.
+ * [namenv] is a mapping from metavar numbers to names, for
+ *          use in instanciating metavars by name.
+ * [env] is the mapping from metavar numbers to their types
+ *       and values.
+ * [hook] is the pointer to the current walking context, for
+ *        integrating existential vars and metavars. *)
 
-type wc = walking_constraints (* Pour une meilleure lisibilité *)
+type wc = walking_constraints (* for a better reading of the following *)
 
 val unify : constr -> tactic
 val unify_0 : 
@@ -54,13 +53,13 @@ val mk_clenv_type_of : wc -> constr -> wc clausenv
 val connect_clenv : wc -> 'a clausenv -> wc clausenv
 val clenv_change_head : constr * constr -> 'a clausenv -> 'a clausenv
 val clenv_assign : int -> constr -> 'a clausenv -> 'a clausenv
-val clenv_instance_term : 'a clausenv -> constr -> constr
+val clenv_instance_term : wc clausenv -> constr -> constr
 val clenv_pose : name * int * constr -> 'a clausenv -> 'a clausenv
 val clenv_template : 'a clausenv -> constr freelisted
 val clenv_template_type : 'a clausenv -> constr freelisted
-val clenv_instance_type : 'a clausenv -> int -> constr
-val clenv_instance_template : 'a clausenv -> constr
-val clenv_instance_template_type : 'a clausenv -> constr
+val clenv_instance_type : wc clausenv -> int -> constr
+val clenv_instance_template : wc clausenv -> constr
+val clenv_instance_template_type : wc clausenv -> constr
 val clenv_unify : constr -> constr -> wc clausenv -> wc clausenv
 val clenv_fchain : int -> 'a clausenv -> wc clausenv -> wc clausenv
 val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic
@@ -68,9 +67,9 @@ val res_pf      : (wc -> tactic) -> wc clausenv -> tactic
 val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic
 val elim_res_pf : (wc -> tactic) -> wc clausenv -> tactic
 val clenv_independent : 
-  'a clausenv -> constr freelisted * constr freelisted -> int list
+  wc clausenv -> constr freelisted * constr freelisted -> int list
 val clenv_missing : 
-  'a clausenv -> constr freelisted * constr freelisted -> int list
+  wc clausenv -> constr freelisted * constr freelisted -> int list
 val clenv_constrain_missing_args : constr list -> wc clausenv -> wc clausenv
 val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
 val clenv_lookup_name : 'a clausenv -> identifier -> int
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e619c70b00..b0823c1b2d 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -21,6 +21,8 @@ type refiner_error =
   | OccurMeta of constr
   | CannotApply of constr * constr
   | CannotUnify of constr * constr
+  | CannotGeneralize of typed_type signature * constr
+  | NotWellTyped of constr
   | BadTacticArgs of string * tactic_arg list
 
 exception RefinerError of refiner_error
diff --git a/proofs/logic.mli b/proofs/logic.mli
index d8c71f7605..59f9cdf69f 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -28,8 +28,8 @@ type refiner_error =
   | OccurMeta of constr
   | CannotApply of constr * constr
   | CannotUnify of constr * constr
+  | CannotGeneralize of typed_type signature * constr
+  | NotWellTyped of constr
   | BadTacticArgs of string * tactic_arg list
 
-exception RefinerError of refiner_error
-
 val error_cannot_unify : path_kind -> constr * constr -> 'a
diff --git a/tactics/pattern.ml b/tactics/pattern.ml
index 8836631fef..297b26bb8e 100644
--- a/tactics/pattern.ml
+++ b/tactics/pattern.ml
@@ -2,15 +2,14 @@
 (* $Id$ *)
 
 open Pp
-open Initial
+open Util
 open Names
 open Generic
 open Term
 open Reduction
-open Termenv
 open Evd
+open Environ
 open Proof_trees
-open Trad
 open Stock
 open Clenv
 
@@ -25,14 +24,17 @@ type module_mark = Stock.module_mark
 type marked_term = constr Stock.stocked
 
 let rec whd_replmeta = function
-  | DOP0(XTRA("ISEVAR",[])) -> DOP0(Meta (newMETA()))
+  | DOP0(XTRA("ISEVAR")) -> DOP0(Meta (new_meta()))
   | DOP2(Cast,c,_) -> whd_replmeta c
   | c -> c
 
 let raw_sopattern_of_compattern sign com =
+  failwith "raw_sopattern_of_compattern: TODO"
+  (***
   let c = Astterm.raw_constr_of_compattern empty_evd (gLOB sign) com in
   strong whd_replmeta c
-    
+  ***)
+
 let parse_pattern s =
   let com =
     try 
@@ -40,7 +42,7 @@ let parse_pattern s =
     with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
       error "Malformed pattern" 
   in
-  raw_sopattern_of_compattern (initial_sign()) com
+  raw_sopattern_of_compattern (Global.context()) com
     
 let (pattern_stock : constr Stock.stock) =
   Stock.make_stock {name="PATTERN";proc=parse_pattern}
@@ -72,15 +74,15 @@ let get_pat = Stock.retrieve pattern_stock
  *)
 
 let dest_soapp_operator = function
-  | DOPN(XTRA("$SOAPP",[]),v) ->
+  | DOPN(XTRA("$SOAPP"),v) ->
       (match Array.to_list v with
 	 | (DOP0(Meta n))::l ->
              let l' = 
 	       List.map (function (Rel i) -> i | _ -> error "somatch") l in
-             Some (n, Listset.uniquize l')
+             Some (n, list_uniquize l')
 	 | _ -> error "somatch")
-  | (DOP2(XTRA("$SOAPP",[]),DOP0(Meta n),Rel p)) ->
-      Some (n,Listset.uniquize [p])
+  | (DOP2(XTRA("$SOAPP"),DOP0(Meta n),Rel p)) ->
+      Some (n,list_uniquize [p])
   | _ -> None
 
 let constrain ((n:int),(m:constr)) sigma =
@@ -93,7 +95,7 @@ let build_dlam toabstract stk (m:constr) =
   let rec buildrec m p_0 p_1 = match p_0,p_1 with 
     | (_, []) -> m
     | (n, (na::tl)) -> 
-	if Listset.mem n toabstract then
+	if List.mem n toabstract then
           buildrec (DLAM(na,m)) (n+1) tl
         else 
 	  buildrec (pop m) (n+1) tl
@@ -102,8 +104,8 @@ let build_dlam toabstract stk (m:constr) =
 
 let memb_metavars m n =
   match (m,n) with
-    | (None, _)       -> true
-    | ((Some mvs), n) -> Listset.mem n mvs
+    | (None, _)     -> true
+    | (Some mvs, n) -> List.mem n mvs
 	  
 let somatch metavars = 
   let rec sorec stk sigma p t =
@@ -111,9 +113,9 @@ let somatch metavars =
     and cT = whd_castapp t in
     match dest_soapp_operator cP with
       | Some (n,ok_args) ->
-          if (not((memb_metavars metavars n))) then error "somatch";
-	  let frels = free_rels cT in
-	  if Listset.subset frels ok_args then 
+          if not (memb_metavars metavars n) then error "somatch";
+	  let frels = Intset.elements (free_rels cT) in
+	  if list_subset frels ok_args then 
 	    constrain (n,build_dlam ok_args stk cT) sigma
 	  else 
 	    error "somatch"
@@ -121,14 +123,15 @@ let somatch metavars =
       | None ->
 	  match (cP,cT) with
        	    | (DOP0(Meta n),m) ->
-		if (not((memb_metavars metavars n))) then
+		if not (memb_metavars metavars n) then
 		  match m with
 		    | DOP0(Meta m_0) -> 
 			if n=m_0 then sigma else error "somatch"
 		    | _ -> error "somatch"
 		else
 		  let depth = List.length stk in
-        	  if Listset.for_all (fun i -> i > depth) (free_rels m) then
+		  let frels = Intset.elements (free_rels m) in
+        	  if List.for_all (fun i -> i > depth) frels then
 		    constrain (n,lift (-depth) m) sigma
         	  else 
 		    error "somatch"
@@ -153,7 +156,7 @@ let somatch metavars =
 	       
   	    | (DOPN(op1,cl1), DOPN(op2,cl2)) ->
 		if op1 = op2 & Array.length cl1 = Array.length cl2 then
-		  it_vect2 (sorec stk) sigma cl1 cl2
+		  array_fold_left2 (sorec stk) sigma cl1 cl2
 		else 
 		  error "somatch"
 
@@ -168,7 +171,7 @@ let somatch metavars =
 		  
   	    | (DLAMV(_,cl1), DLAMV(na,cl2)) ->
 		if Array.length cl1 = Array.length cl2 then
-		  it_vect2 (sorec (na::stk)) sigma cl1 cl2
+		  array_fold_left2 (sorec (na::stk)) sigma cl1 cl2
 		else 
 		  error "somatch"
 		    
@@ -178,19 +181,20 @@ let somatch metavars =
 
 let somatches n pat =
   let m = get_pat pat in 
-  try somatch None m n; true with UserError _ -> false
+  try let _ = somatch None m n in true with UserError _ -> false
 
 let dest_somatch n pat =
-  let m    = get_pat pat in
-  let mvs  = collect_metas m in
-  let mvb  = somatch (Some (Listset.uniquize mvs)) m n in
+  let m = get_pat pat in
+  let mvs = collect_metas m in
+  let mvb = somatch (Some (list_uniquize mvs)) m n in
   List.map (fun b -> List.assoc b mvb) mvs
 
 let soinstance pat arglist =
-  let m =   get_pat pat in
+  let m = get_pat pat in
   let mvs = collect_metas m in
   let mvb = List.combine mvs arglist in 
-  Sosub.soexecute (Reduction.strong (Reduction.whd_meta mvb) m)
+  Sosub.soexecute (Reduction.strong (fun _ _ -> Reduction.whd_meta mvb) 
+		     empty_env Evd.empty m)
 
 (* I implemented the following functions which test whether a term t
    is an inductive but non-recursive type, a general conjuction, a
@@ -200,9 +204,7 @@ let soinstance pat arglist =
    since they do not depend on the name of the type. Hence, they 
    also work on ad-hoc disjunctions introduced by the user.
   
-  -- Eduardo (6/8/97).
-
- *)
+  -- Eduardo (6/8/97). *)
 
 let mmk = make_module_marker ["Prelude"]
 
@@ -216,9 +218,9 @@ let match_with_non_recursive_type t =
   match kind_of_term t with 
     | IsAppL _ -> 
         let (hdapp,args) = decomp_app t in
-        (match (kind_of_term hdapp) with
+        (match kind_of_term hdapp with
            | IsMutInd _ -> 
-               if not (mind_is_recursive hdapp) then 
+               if not (Global.mind_is_recursive hdapp) then 
 		 Some (hdapp,args) 
 	       else 
 		 None 
@@ -234,10 +236,10 @@ let match_with_conjunction t =
   let (hdapp,args) = decomp_app t in 
   match kind_of_term hdapp with
     | IsMutInd _ -> 
-        let nconstr = mis_nconstr (mind_specif_of_mind hdapp) in  
+        let nconstr = Global.mind_nconstr hdapp in  
 	if (nconstr = 1) && 
-          (not (mind_is_recursive hdapp)) &&
-          (nb_prod (mind_arity hdapp))=(mind_nparams hdapp)
+          (not (Global.mind_is_recursive hdapp)) &&
+          (nb_prod (Global.mind_arity hdapp)) = (Global.mind_nparams hdapp)
         then 
 	  Some (hdapp,args)
         else 
@@ -254,10 +256,11 @@ let match_with_disjunction t =
   match kind_of_term hdapp with
     | IsMutInd _  -> 
         let constr_types = 
-	  mis_lc_without_abstractions (mind_specif_of_mind hdapp) in
-        let only_one_arg c = ((nb_prod c) - (mind_nparams hdapp)) = 1 in 
-	if (Vectops.for_all_vect only_one_arg constr_types) &&
-          (not (mind_is_recursive hdapp))
+	  Global.mind_lc_without_abstractions hdapp in
+        let only_one_arg c = 
+	  ((nb_prod c) - (Global.mind_nparams hdapp)) = 1 in 
+	if (array_for_all only_one_arg constr_types) &&
+          (not (Global.mind_is_recursive hdapp))
         then 
 	  Some (hdapp,args)
         else 
@@ -270,7 +273,7 @@ let match_with_empty_type t =
   let (hdapp,args) = decomp_app t in
   match (kind_of_term hdapp) with
     | IsMutInd _ -> 
-        let nconstr = mis_nconstr (mind_specif_of_mind hdapp) in  
+        let nconstr = Global.mind_nconstr hdapp in  
 	if nconstr = 0 then Some hdapp else None
     | _ ->  None
 	  
@@ -281,10 +284,10 @@ let match_with_unit_type t =
   match (kind_of_term hdapp) with
     | IsMutInd _  -> 
         let constr_types = 
-	  mis_lc_without_abstractions (mind_specif_of_mind hdapp) in 
-        let nconstr = mis_nconstr (mind_specif_of_mind hdapp) in
-        let zero_args c = ((nb_prod c) - (mind_nparams hdapp)) = 0 in  
-	if nconstr = 1 && (Vectops.for_all_vect zero_args constr_types) then 
+	  Global.mind_lc_without_abstractions hdapp in 
+        let nconstr = Global.mind_nconstr hdapp in
+        let zero_args c = ((nb_prod c) - (Global.mind_nparams hdapp)) = 0 in  
+	if nconstr = 1 && (array_for_all zero_args constr_types) then 
 	  Some hdapp
         else 
 	  None
@@ -302,10 +305,10 @@ let match_with_equation  t =
   match (kind_of_term hdapp) with
     | IsMutInd _  -> 
         let constr_types = 
-	  mis_lc_without_abstractions (mind_specif_of_mind hdapp) in 
+	  Global.mind_lc_without_abstractions hdapp in 
         let refl_rel_term1 = put_pat mmk "(A:?)(x:A)(? A x x)" in
         let refl_rel_term2 = put_pat mmk "(x:?)(? x x)" in
-        let nconstr = mis_nconstr (mind_specif_of_mind hdapp) in
+        let nconstr = Global.mind_nconstr hdapp in
 	if nconstr = 1 &&
            (somatches constr_types.(0) refl_rel_term1 ||
             somatches constr_types.(0) refl_rel_term2) 
diff --git a/tactics/pattern.mli b/tactics/pattern.mli
index e39ecf9ec8..4cfb482564 100644
--- a/tactics/pattern.mli
+++ b/tactics/pattern.mli
@@ -46,9 +46,9 @@ val make_module_marker : string list -> module_mark
 val put_pat            : module_mark -> string -> marked_term
 val get_pat            : marked_term -> constr
 val pattern_stock      : constr Stock.stock
-(***
+(*i**
 val raw_sopattern_of_compattern : typed_type signature -> CoqAst.t -> constr
-***)
+**i*)
 
 (*s Second part : Given a term with second-order variables in it,
    represented by Meta's, and possibly applied using \verb!XTRA[$SOAPP]! to
@@ -70,7 +70,7 @@ val raw_sopattern_of_compattern : typed_type signature -> CoqAst.t -> constr
    contained in the arguments of the application, and in that case, we
    construct a [DLAM] with the names on the stack. *)
 
-val somatch      : Intset.t option -> constr -> constr -> constr Intmap.t
+val somatch      : int list option -> constr -> constr -> (int * constr) list
 val somatches    : constr -> marked_term -> bool
 val dest_somatch : constr -> marked_term -> constr list
 val soinstance   : marked_term -> constr list -> constr 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 56cd5a42f9..49c384df4a 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -190,7 +190,7 @@ fois pour toutes : en particulier si Pattern.somatch produit une UserError
 Ce qui fait que si la conclusion ne matche pas le pattern, Auto échoue, même
 si après Intros la conclusion matche le pattern.
 *)
-(***
+(***TODO
 let conclPattern concl pat tacast gl = 
   let constr_bindings = Pattern.somatch None pat concl in
   let ast_bindings = 
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
new file mode 100644
index 0000000000..44f17e8165
--- /dev/null
+++ b/tactics/wcclausenv.ml
@@ -0,0 +1,207 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Sign
+open Reduction
+open Environ
+open Logic
+open Tacmach
+open Evd
+open Proof_trees
+open Clenv
+
+(* If you have a precise idea of the intended use of the following code, please
+   write to Eduardo.Gimenez@inria.fr and ask for the prize :-)
+   -- Eduardo (11/8/97) *)
+
+let pf_get_new_id id gls = 
+  next_ident_away id (ids_of_sign (pf_untyped_hyps gls))
+
+let pf_get_new_ids ids gls =
+  let avoid = ids_of_sign (pf_untyped_hyps gls) in
+  List.fold_right
+    (fun id acc -> (next_ident_away id (acc@avoid))::acc)
+    ids []
+
+type arg_binder =
+  | Dep of identifier
+  | Nodep of int
+  | Abs of int
+
+type arg_bindings = (arg_binder * constr) list
+
+let clenv_constrain_with_bindings bl clause =
+  if bl = [] then 
+    clause 
+  else 
+    let all_mvs = collect_metas (clenv_template clause).rebus
+    and ind_mvs = clenv_independent clause
+		    (clenv_template clause,
+                     clenv_template_type clause) in
+    let nb_indep = List.length ind_mvs in
+    let rec matchrec clause = function
+      | []       -> clause
+      | (b,c)::t ->
+          let k = 
+            match b with
+              | Dep s ->
+		  if List.mem_assoc b t then 
+		    errorlabstrm "clenv_match_args" 
+                      [< 'sTR "The variable "; print_id s; 
+			 'sTR " occurs more than once in binding" >];
+		  clenv_lookup_name clause s
+              | Nodep n ->
+		  let index = if n > 0 then n-1 else nb_indep+n in
+                  if List.mem_assoc (Nodep (index+1)) t or 
+                    List.mem_assoc (Nodep (index-nb_indep)) t
+                  then errorlabstrm "clenv_match_args"
+                    [< 'sTR "The position "; 'iNT n ;
+		       'sTR " occurs more than once in binding" >];
+		  (try 
+		     List.nth ind_mvs index
+		   with Failure _ ->
+                     errorlabstrm "clenv_constrain_with_bindings"
+                       [< 'sTR"Clause did not have " ; 'iNT n ; 'sTR"-th" ;
+                          'sTR" unnamed argument" >])
+              | Abs n -> 
+                  (try
+                     if n > 0 then 
+		       List.nth all_mvs (n-1)
+                     else if n < 0 then 
+		       List.nth (List.rev all_mvs) (-n-1)
+                     else error "clenv_constrain_with_bindings" 
+                   with Failure _ ->
+                     errorlabstrm "clenv_constrain_with_bindings"
+                       [< 'sTR"Clause did not have " ; 'iNT n ; 'sTR"-th" ;
+                          'sTR" absolute argument" >])
+	  in
+	  let env = Global.unsafe_env () in
+	  let sigma = Evd.empty in
+	  let k_typ = nf_betaiota env sigma (clenv_instance_type clause k) in
+	  let c_typ = nf_betaiota env sigma (w_type_of clause.hook c) in 
+	  matchrec (clenv_assign k c (clenv_unify k_typ c_typ clause)) t
+    in 
+    matchrec clause bl
+
+(***TODO: SUPPRIMMER ??
+let add_prod_rel sigma (t,env) =
+  match t with
+    | DOP2(Prod,c1,(DLAM(na,b))) ->
+        (b,add_rel (na,Typing_ev.execute_type sigma env c1) env)
+    | _ -> failwith "add_prod_rel"
+
+let rec add_prods_rel sigma (t,env) =
+  try 
+    add_prods_rel sigma (add_prod_rel sigma (whd_betadeltaiota sigma t,env))
+  with Failure "add_prod_rel" -> 
+    (t,env)
+
+let add_prod_sign sigma (t,sign) =
+  match t with
+    | DOP2(Prod,c1,(DLAM(na,_) as b)) ->
+        let id = Environ.id_of_name_using_hdchar t na in  
+	(sAPP b (VAR id),
+         add_sign (id, fexecute_type sigma sign c1) sign)
+    | _ -> failwith "add_prod_sign"
+
+let rec add_prods_sign sigma (t,sign) =
+  try 
+    add_prods_sign sigma (add_prod_sign sigma (whd_betadeltaiota sigma t,sign))
+  with Failure "add_prod_sign" -> 
+    (t,sign)
+***)
+
+(* What follows is part of the contents of the former file tactics3.ml *)
+    
+let res_pf_THEN kONT clenv tac gls =
+  let clenv' = (clenv_unique_resolver false clenv gls) in 
+  (tclTHEN (clenv_refine kONT clenv') (tac clenv')) gls
+
+let res_pf_THEN_i kONT clenv tac i gls =
+  let clenv' = (clenv_unique_resolver false clenv gls) in 
+  tclTHEN_i (clenv_refine kONT clenv') (tac clenv') i gls
+
+let elim_res_pf_THEN_i kONT clenv tac i gls =  
+  let clenv' = (clenv_unique_resolver true clenv gls) in
+  tclTHEN_i (clenv_refine kONT clenv') (tac clenv') i gls
+
+let rec build_args acc ce p_0 p_1 =
+  match p_0,p_1 with 
+    | ((DOP2(Prod,a,(DLAM(na,_) as b))), (a_0::bargs)) ->
+        let (newa,ce') = (build_term ce (na,Some a) a_0) in 
+	build_args (newa::acc) ce' (sAPP b a_0) bargs
+    | (_, [])     -> (List.rev acc,ce)
+    | (_, (_::_)) -> failwith "mk_clenv_using"
+
+and build_term ce p_0 p_1 =
+  let env = Global.unsafe_env() in
+  match p_0,p_1 with 
+    | ((na,Some t), (DOP0(Meta mv))) -> 
+        build_term ce (na,Some t) mkExistential
+    | ((na,Some t), (DOP0(XTRA("ISEVAR")))) ->
+    	let mv = new_meta() in 
+	(DOP0(Meta mv),
+         clenv_pose (na,mv,t) ce)
+    | ((na,_), (DOP2(Cast,c,t))) -> build_term ce (na,Some t) c
+    | ((na,Some t), c) ->
+    	if (not((occur_meta c))) then 
+	  (c,ce)
+    	else 
+	  let (hd,args) = 
+	    whd_betadeltaiota_stack env (w_Underlying ce.hook) c [] in
+          let hdty = w_type_of ce.hook hd in
+          let (args,ce') =
+	    build_args [] ce (w_whd_betadeltaiota ce.hook hdty) args in
+          let newc = applist(hd,args) in
+          let t' = clenv_type_of ce' newc in  
+	  if w_conv_x ce'.hook t t' then 
+	    (newc,ce') 
+	  else 
+	    failwith "mk_clenv_using"
+    | ((na,None), c) ->
+    	if (not((occur_meta c))) then 
+	  (c,ce)
+    	else 
+	  let (hd,args) = 
+	    whd_betadeltaiota_stack env (w_Underlying ce.hook) c [] in
+          let hdty = w_type_of ce.hook hd in
+          let (args,ce') = 
+	    build_args [] ce (w_whd_betadeltaiota ce.hook hdty) args in
+          let newc = applist(hd,args) in
+	  (newc,ce')
+
+let mk_clenv_using wc c =
+  let ce = mk_clenv wc mkImplicit in
+  let (newc,ce') = 
+    try 
+      build_term ce (Anonymous,None) c
+    with Failure _ -> 
+      raise (RefinerError (NotWellTyped c))
+  in
+  clenv_change_head (newc,clenv_type_of ce' newc) ce'
+
+let applyUsing c gl =
+  let (wc,kONT) = startWalk gl in
+  let clause = mk_clenv_using wc c in 
+  res_pf kONT clause gl
+
+let clenv_apply_n_times n ce =
+  let templtyp = clenv_instance_template_type ce
+  and templval = (clenv_template ce).rebus in   
+  let rec apprec ce argacc (n,ty) =
+    let env = Global.unsafe_env () in
+    match (n, whd_betadeltaiota env (w_Underlying ce.hook) ty) with 
+      | (0, templtyp) ->
+	  clenv_change_head (applist(templval,List.rev argacc), templtyp) ce
+      | (n, (DOP2(Prod,dom,DLAM(na,rng)))) ->
+          let mv = new_meta() in
+          let newce = clenv_pose (na,mv,dom) ce in
+	  apprec newce (mkMeta mv::argacc) (n-1, subst1 (mkMeta mv) rng)
+      | (n, _) -> failwith "clenv_apply_n_times"
+  in 
+  apprec ce [] (n, templtyp)
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index 88d14d3602..3cea47392d 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -24,6 +24,7 @@ type arg_bindings = (arg_binder * constr) list
 val clenv_constrain_with_bindings :
   arg_bindings -> walking_constraints clausenv -> walking_constraints clausenv
 
+(*i**
 val add_prod_rel : 'a evar_map -> constr * context -> constr * context
 
 val add_prods_rel : 'a evar_map -> constr * context -> constr * context
@@ -33,6 +34,7 @@ val add_prod_sign :
 
 val add_prods_sign : 
   'a evar_map -> constr * typed_type signature -> constr * typed_type signature
+**i*)
 
 val res_pf_THEN         : (walking_constraints -> tactic) -> 
                            walking_constraints clausenv ->