Introduction d'un type constr_pattern pour les différents filtrages

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

21 files changed, 516 insertions, 296 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 844e364316..737f6a2e1a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -117,7 +117,7 @@ type rhs =
 
 type equation =
     { dependencies : constr lifted list;
-      patterns     : pattern list; 
+      patterns     : cases_pattern list; 
       rhs          : rhs;
       tag          : pattern_source }
 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index ec43265658..ab3075f453 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -2,6 +2,7 @@
 (* $Id$ *)
 
 (*i*)
+open Util
 open Names
 open Sign
 open Type_errors
@@ -13,29 +14,30 @@ type loc = int * int
 
 (* locs here refers to the ident's location, not whole pat *)
 (* the last argument of PatCstr is a possible alias ident for the pattern *)
-type pattern =
+type cases_pattern =
   | PatVar of loc * name
-  | PatCstr of loc * (constructor_path * identifier list) * pattern list * name
+  | PatCstr of
+      loc * (constructor_path * identifier list) * cases_pattern list * name
 
 type binder_kind = BProd | BLambda
 type fix_kind = RFix of int array * int | RCofix of int
 type rawsort = RProp of Term.contents | RType
 
-type reference =
-  | RConst of section_path * identifier list
-  | RInd of inductive_path * identifier list
-  | RConstruct of constructor_path * identifier list
+type 'ctxt reference =
+  | RConst of section_path * 'ctxt
+  | RInd of inductive_path * 'ctxt
+  | RConstruct of constructor_path * 'ctxt
   | RAbst of section_path
   | RVar of identifier
-  | REVar of int * identifier list
+  | REVar of int * 'ctxt
   | RMeta of int
 
 type rawconstr = 
-  | RRef of loc * reference
+  | RRef of loc * rawconstr array reference
   | RApp of loc * rawconstr * rawconstr list
   | RBinder of loc * binder_kind * name * rawconstr * rawconstr
   | RCases of loc * Term.case_style * rawconstr option * rawconstr list * 
-      (identifier list * pattern list * rawconstr) list
+      (identifier list * cases_pattern list * rawconstr) list
   | ROldCase of loc * bool * rawconstr option * rawconstr * 
       rawconstr array
   | RRec of loc * fix_kind * identifier array * 
@@ -69,3 +71,70 @@ let loc_of_rawconstr = function
   | RHole (Some loc) -> loc
   | RHole (None) -> dummy_loc
   | RCast (loc,_,_) -> loc
+
+type constr_pattern =
+  | PRef of constr_pattern array reference
+  | PRel of int
+  | PApp of constr_pattern * constr_pattern array
+  | PSoApp of int * int list
+  | PBinder of binder_kind * name * constr_pattern * constr_pattern
+  | PSort of rawsort
+  | PMeta of int
+(*
+  | PCast of loc * constr_pattern * constr_pattern
+  | PCases of loc * Term.case_style * constr_pattern option * constr_pattern list * 
+      (identifier list * pattern list * constr_pattern) list
+  | POldCase of loc * bool * constr_pattern option * constr_pattern * 
+      constr_pattern array
+  | Pec of loc * fix_kind * identifier array * 
+      constr_pattern array * constr_pattern array
+*)
+
+let rec occur_meta_pattern = function
+  | PApp (f,args) ->
+      (occur_meta_pattern f) or (array_exists occur_meta_pattern args)
+  | PBinder(_,na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
+  | PMeta _ | PSoApp _ -> true
+  | PRel _ | PSort _   -> false
+
+  (* On suppose que les ctxt des cstes ne contient pas de meta *)
+  | PRef _             -> false
+
+type constr_label =
+  | ConstNode of section_path
+  | IndNode of inductive_path
+  | CstrNode of constructor_path
+  | VarNode of identifier
+(*
+  | ... 
+*)
+
+exception BoundPattern;;
+
+let label_of_ref = function
+  | RConst (sp,_)     -> ConstNode sp
+  | RInd (sp,_)       -> IndNode sp
+  | RConstruct (sp,_) -> CstrNode sp
+  | RVar id           -> VarNode id
+  | RAbst _           -> error "Obsolète"
+  | REVar _ | RMeta _ -> raise BoundPattern
+
+let rec head_pattern_bound t =
+  match t with
+    | PBinder (BProd,_,_,b) -> head_pattern_bound b 
+    | PApp (f,args)         -> head_pattern_bound f
+    | PRef r                -> label_of_ref r
+    | PRel _ | PMeta _ | PSoApp _  | PSort _ -> raise BoundPattern
+    | PBinder(BLambda,_,_,_) -> anomaly "head_pattern_bound: not a type"
+
+open Generic
+open Term
+
+let head_of_constr_reference = function
+  | DOPN (Const sp,_) -> ConstNode sp
+  | DOPN (MutConstruct sp,_) -> CstrNode sp
+  | DOPN (MutInd sp,_) -> IndNode sp
+  | VAR id -> VarNode id
+  | _ -> anomaly "Not a rigid reference"
+
+
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index c31691046d..f78520a16f 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -13,29 +13,30 @@ type loc = int * int
 
 (* locs here refers to the ident's location, not whole pat *)
 (* the last argument of PatCstr is a possible alias ident for the pattern *)
-type pattern =
+type cases_pattern =
   | PatVar of loc * name
-  | PatCstr of loc * (constructor_path * identifier list) * pattern list * name
+  | PatCstr of
+      loc * (constructor_path * identifier list) * cases_pattern list * name
 
 type binder_kind = BProd | BLambda
 type fix_kind = RFix of int array * int | RCofix of int
 type rawsort = RProp of Term.contents | RType
 
-type reference =
-  | RConst of section_path * identifier list
-  | RInd of inductive_path * identifier list
-  | RConstruct of constructor_path * identifier list
+type 'ctxt reference =
+  | RConst of section_path * 'ctxt
+  | RInd of inductive_path * 'ctxt
+  | RConstruct of constructor_path * 'ctxt
   | RAbst of section_path
   | RVar of identifier
-  | REVar of int * identifier list
+  | REVar of int * 'ctxt
   | RMeta of int
 
 type rawconstr = 
-  | RRef of loc * reference
+  | RRef of loc * rawconstr array reference
   | RApp of loc * rawconstr * rawconstr list
   | RBinder of loc * binder_kind * name * rawconstr * rawconstr
   | RCases of loc * Term.case_style * rawconstr option * rawconstr list * 
-      (identifier list * pattern list * rawconstr) list
+      (identifier list * cases_pattern list * rawconstr) list
   | ROldCase of loc * bool * rawconstr option * rawconstr * 
       rawconstr array
   | RRec of loc * fix_kind * identifier array * 
@@ -58,3 +59,33 @@ i*)
 
 val dummy_loc : loc
 val loc_of_rawconstr : rawconstr -> loc
+
+type constr_pattern =
+  | PRef of constr_pattern array reference
+  | PRel of int
+  | PApp of constr_pattern * constr_pattern array
+  | PSoApp of int * int list
+  | PBinder of binder_kind * name * constr_pattern * constr_pattern
+  | PSort of rawsort
+  | PMeta of int
+
+val occur_meta_pattern : constr_pattern -> bool
+
+type constr_label =
+  | ConstNode of section_path
+  | IndNode of inductive_path
+  | CstrNode of constructor_path
+  | VarNode of identifier
+
+(* [head_pattern_bound t] extracts the head variable/constant of the
+   type [t] or raises [BoundPattern] (even if a sort); it raises an anomaly
+   if [t] is an abstraction *)
+
+exception BoundPattern
+val head_pattern_bound : constr_pattern -> constr_label
+
+(* [head_of_constr_reference c] assumes [r] denotes a reference and
+   returns its label; raises an anomaly otherwise *)
+
+val head_of_constr_reference : Term.constr -> constr_label
+
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0084e96f3f..1e13cb577e 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -538,53 +538,87 @@ let clenv_wtactic wt clenv =
     env = clenv.env;
     hook = wt clenv.hook }
 
+let clenv_type_of ce c =
+  Typing.type_of (w_env ce.hook) (w_Underlying ce.hook) c
+  (***
+  let metamap =
+    List.map 
+      (function
+	 | (n,Clval(_,typ)) -> (n,typ.rebus)
+         | (n,Cltyp typ)    -> (n,typ.rebus))
+      (intmap_to_list ce.env)
+  in
+  (Pretyping.ise_resolve true (w_Underlying ce.hook) metamap
+     (gLOB(w_hyps ce.hook)) c).uj_type
+  ***)
+
+let clenv_instance_type_of ce c =
+  clenv_instance ce (mk_freelisted (clenv_type_of ce c))
+
+(* [clenv_merge b metas evars clenv] merges common instances in metas
+   or in evars, possibly generating new unification problems; if [b]
+   is true, unification of types of metas is required *)
+
+let clenv_merge with_types =
+  let rec clenv_resrec metas evars clenv =
+    match (evars,metas) with
+      | ([],[]) -> clenv
+
+      | ((lhs,(DOP0(Meta k) as rhs))::t,metas) ->
+    	  clenv_resrec ((k,lhs)::metas) t clenv
+
+      | ((DOPN(Evar evn,_) as evar,rhs)::t,metas) ->
+    	  if w_defined_const clenv.hook evar then
+            let (metas',evars') = unify_0 [] clenv.hook rhs evar in
+            clenv_resrec (metas'@metas) (evars'@t) clenv
+    	  else
+            (try 
+	       clenv_resrec metas t (clenv_wtactic (w_Define evn rhs) clenv)
+             with ex when catchable_exception ex ->
+               (match rhs with
+		  | DOPN(AppL,cl) ->
+		      (match cl.(0) with
+			 | (DOPN(Const _,_) | DOPN(MutConstruct _,_)) ->
+			     clenv_resrec metas evars 
+			       (clenv_wtactic (mimick_evar cl.(0) 
+						 ((Array.length cl) - 1) evn) 
+				  clenv)
+			 | _ -> error "w_Unify")
+           	  | _ -> error "w_Unify"))
+      | ([],(mv,n)::t) ->
+    	  if clenv_defined clenv mv then
+            let (metas',evars') =
+              unify_0 [] clenv.hook (clenv_value clenv mv).rebus n in
+            clenv_resrec (metas'@t) evars' clenv
+    	  else
+	    let mc,ec =
+	      if with_types then
+		let nty = clenv_type_of clenv 
+			    (clenv_instance clenv (mk_freelisted n)) in
+		unify_0 [] clenv.hook (clenv_instance_type clenv mv) nty
+	      else ([],[]) in
+	    clenv_resrec (mc@t) ec (clenv_assign mv n clenv)
+
+      | _ -> anomaly "clenv_resrec"
+
+  in clenv_resrec
 
 (* [clenv_unify M N clenv]
- * performs a unification of M and N, generating a bunch of
- * unification constraints in the process.  These constraints
- * are processed, one-by-one - they may either generate new
- * bindings, or, if there is already a binding, new unifications,
- * which themselves generate new constraints.  This continues
- * until we get failure, or we run out of constraints. *)
-
-let rec clenv_unify m n clenv =
+   performs a unification of M and N, generating a bunch of
+   unification constraints in the process.  These constraints
+   are processed, one-by-one - they may either generate new
+   bindings, or, if there is already a binding, new unifications,
+   which themselves generate new constraints.  This continues
+   until we get failure, or we run out of constraints.
+   [clenv_typed_unify M N clenv] expects in addition that expected
+   types of metavars are unifiable with the types of their instances    *)
+
+let clenv_unify_core with_types m n clenv =
   let (mc,ec) = unify_0 [] clenv.hook m n in 
-  clenv_resrec mc ec clenv
+  clenv_merge with_types mc ec clenv
     
-and clenv_resrec metas evars clenv =
-  match (evars,metas) with
-    | ([],[]) -> clenv
-	  
-    | ((lhs,(DOP0(Meta k) as rhs))::t,metas) ->
-    	clenv_resrec ((k,lhs)::metas) t clenv
-	  
-    | ((DOPN(Evar evn,_) as evar,rhs)::t,metas) ->
-    	if w_defined_const clenv.hook evar then
-          let (metas',evars') = unify_0 [] clenv.hook rhs evar in
-          clenv_resrec (metas'@metas) (evars'@t) clenv
-    	else
-          (try 
-	     clenv_resrec metas t (clenv_wtactic (w_Define evn rhs) clenv)
-           with ex when catchable_exception ex ->
-             (match rhs with
-		| DOPN(AppL,cl) ->
-		    (match cl.(0) with
-		       | (DOPN(Const _,_) | DOPN(MutConstruct _,_)) ->
-			   clenv_resrec metas evars 
-			     (clenv_wtactic (mimick_evar cl.(0) 
-					       ((Array.length cl) - 1) evn) 
-				clenv)
-		       | _ -> error "w_Unify")
-           	| _ -> error "w_Unify"))
-    | ([],(mv,n)::t) ->
-    	if clenv_defined clenv mv then
-          let (metas',evars') =
-            unify_0 [] clenv.hook (clenv_value clenv mv).rebus n in
-          clenv_resrec (metas'@t) evars' clenv
-    	else 
-	  clenv_resrec t [] (clenv_assign mv n clenv)
-    | _ -> anomaly "clenv_resrec"
-	  
+let clenv_unify = clenv_unify_core false
+let clenv_typed_unify = clenv_unify_core true
 
 (* [clenv_bchain mv clenv' clenv]
  *
@@ -885,76 +919,6 @@ let clenv_add_sign (id,sign) clenv =
     env = clenv.env;
     hook = w_add_sign (id,sign) clenv.hook}
 
-let clenv_type_of ce c =
-  Typing.type_of (w_env ce.hook) (w_Underlying ce.hook) c
-  (***
-  let metamap =
-    List.map 
-      (function
-	 | (n,Clval(_,typ)) -> (n,typ.rebus)
-         | (n,Cltyp typ)    -> (n,typ.rebus))
-      (intmap_to_list ce.env)
-  in
-  (Pretyping.ise_resolve true (w_Underlying ce.hook) metamap
-     (gLOB(w_hyps ce.hook)) c).uj_type
-  ***)
-
-let clenv_instance_type_of ce c =
-  clenv_instance ce (mk_freelisted (clenv_type_of ce c))
-
-(* [clenv_typed_unify gls M N clenv]
- * peforms a unification of M and N, generating a bunch of
- * unification constraints in the process.  These constraints
- * are processed, one-by-one - they may either generate new
- * bindings, or, if there is already a binding, new unifications,
- * which themselves generate new constraints.  This continues
- * until we get failure, or we run out of constraints. *)
-
-let rec clenv_typed_unify m n clenv =
-  let (mc,ec) = unify_0 [] clenv.hook m n in 
-  clenv_resrec mc ec clenv
-
-and clenv_resrec metas evars clenv =
-  match (evars,metas) with
-    | ([],[]) -> clenv
-	  
-    | ((lhs,(DOP0(Meta k) as rhs))::t,metas) ->
-    	clenv_resrec ((k,lhs)::metas) t clenv
-
-    | ((DOPN(Evar evn,_) as evar,rhs)::t,metas) ->
-    	if w_defined_const clenv.hook evar then
-          let (metas',evars') = unify_0 [] clenv.hook rhs evar in
-          clenv_resrec (metas'@metas) (evars'@t) clenv
-    	else
-          (try 
-	     clenv_resrec metas t (clenv_wtactic (w_Define evn rhs) clenv)
-           with ex when catchable_exception ex ->
-             (match rhs with
-		| DOPN(AppL,cl) ->
-		    (match cl.(0) with
-		       | (DOPN(Const _,_) |  DOPN(MutConstruct _,_)) ->
-			   clenv_resrec metas evars 
-			     (clenv_wtactic (mimick_evar cl.(0) 
-					       ((Array.length cl) - 1) evn) 
-				clenv)
-		       | _ -> error "w_Unify")
-           	| _ -> error "w_Unify"))
-	  
-    | ([],(mv,n)::t) ->
-    	if clenv_defined clenv mv then
-          let (metas',evars') =
-            unify_0 [] clenv.hook (clenv_value clenv mv).rebus n in
-          clenv_resrec (metas'@t) evars' clenv
-    	else 
-	  let nty = clenv_type_of clenv 
-		      (clenv_instance clenv (mk_freelisted n)) in
-	  let (mc,ec) =
-	    unify_0 [] clenv.hook (clenv_instance_type clenv mv) nty in
-	  clenv_resrec (mc@t) ec (clenv_assign mv n clenv)
-
-    | _ -> anomaly "clenv_resrec"
-
-
 (* The unique unification algorithm works like this: If the pattern is
    flexible, and the goal has a lambda-abstraction at the head, then
    we do a first-order unification.
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 97222bd359..7d9d3530af 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -14,6 +14,7 @@ open Typing
 open Tacmach
 open Proof_trees
 open Pfedit
+open Rawterm
 open Tacred
 open Tactics
 open Tacticals
@@ -39,7 +40,7 @@ type auto_tactic =
 type pri_auto_tactic = { 
   hname : identifier;    (* name of the hint *)
   pri  : int;            (* A number between 0 and 4, 4 = lower priority *)
-  pat  : constr option;  (* A pattern for the concl of the Goal *)
+  pat  : constr_pattern option; (* A pattern for the concl of the Goal *)
   code : auto_tactic     (* the tactic to apply when the concl matches pat *)
 }
 
@@ -88,7 +89,7 @@ let lookup_tacs (hdc,c) (l,l',dn) =
 
 
 module Constr_map = Map.Make(struct 
-			       type t = constr 
+			       type t = constr_label
 			       let compare = Pervasives.compare 
 			     end)
 
@@ -182,20 +183,25 @@ let rec nb_hyp = function
 
 (* adding and removing tactics in the search table *)
 
+let try_head_pattern c = 
+  try head_pattern_bound c
+  with BoundPattern -> error "Bound head variable"
+
 let make_exact_entry name (c,cty) =
   match strip_outer_cast cty with
     | DOP2(Prod,_,_) -> 
 	failwith "make_exact_entry"
-    | cty -> 
-	(List.hd (head_constr cty),
-	 { hname=name; pri=0; pat=None; code=Give_exact c })
+    | cty ->
+	(head_of_constr_reference (List.hd (head_constr cty)),
+	   { hname=name; pri=0; pat=None; code=Give_exact c })
 
 let make_apply_entry (eapply,verbose) name (c,cty) =
   match hnf_constr (Global.env()) Evd.empty cty with
     | DOP2(Prod,_,_) as cty ->
-        let hdconstr = (try  List.hd (head_constr_bound cty [])  
-                        with Bound -> failwith "make_apply_entry") in
-        let ce = mk_clenv_from () (c,cty) in 
+        let ce = mk_clenv_from () (c,cty) in
+	let pat = Pattern.pattern_of_constr (clenv_template_type ce).rebus in
+        let hd = (try head_pattern_bound pat
+                  with BoundPattern -> failwith "make_apply_entry") in
         let nmiss = 
 	  List.length 
             (clenv_missing ce (clenv_template ce,clenv_template_type ce)) 
@@ -204,16 +210,16 @@ let make_apply_entry (eapply,verbose) name (c,cty) =
           if verbose then 
 	    wARN [< 'sTR "the hint: EApply "; prterm c;
 		    'sTR " will only be used by EAuto" >]; 
-          (hdconstr,
+          (hd,
            { hname = name;
 	     pri = nb_hyp cty + nmiss;
-             pat = Some (clenv_template_type ce).rebus;
+             pat = Some pat;
              code = ERes_pf(c,ce) })
         end else 
-	  (hdconstr,
+	  (hd,
            { hname = name;
 	     pri = nb_hyp cty;
-             pat = Some (clenv_template_type ce).rebus;
+             pat = Some pat;
              code = Res_pf(c,ce) })
     | _ -> failwith "make_apply_entry"
  
@@ -263,7 +269,7 @@ let make_unfold (hintname, id) =
      with Not_found -> 
        errorlabstrm  "make_unfold" [<print_id id; 'sTR " not declared" >])
   in 
-  (hdconstr, 
+  (head_of_constr_reference hdconstr, 
    { hname = hintname;
      pri = 4;
      pat = None;
@@ -276,18 +282,17 @@ let add_unfolds l dbnames =
     dbnames
 
 let make_extern name pri pat tacast = 
-  let hdconstr = List.hd (head_constr pat) in 
+  let hdconstr = try_head_pattern pat in 
   (hdconstr,
    { hname = name;
      pri=pri;
      pat = Some pat;
      code= Extern tacast })
 
-let add_extern name pri pat tacast dbname =
+let add_extern name pri (patmetas,pat) tacast dbname =
   (* We check that all metas that appear in tacast have at least
      one occurence in the left pattern pat *)
   let tacmetas = Coqast.collect_metas tacast in 
-  let patmetas = Clenv.collect_metas pat in
   match (list_subtract tacmetas patmetas) with
     | i::_ ->
 	errorlabstrm "add_extern" 
@@ -302,11 +307,11 @@ let add_externs name pri pat tacast dbnames =
 let make_trivial (name,c) =
   let sigma = Evd.empty and env = Global.env() in
   let t = type_of env sigma c in
-  let hdconstr = List.hd (head_constr t) in
+  let hd = head_of_constr_reference (List.hd (head_constr t)) in
   let ce = mk_clenv_from () (c,hnf_constr env sigma t) in
-  (hdconstr, { hname = name;
+  (hd, { hname = name;
 	       pri=1;
-               pat = Some(clenv_template_type ce).rebus;
+               pat = Some (Pattern.pattern_of_constr (clenv_template_type ce).rebus);
                code=Res_pf_THEN_trivial_fail(c,ce) })
 
 let add_trivials l dbnames =
@@ -378,8 +383,8 @@ let _ =
     (function 
        | [VARG_IDENTIFIER hintname; VARG_VARGLIST l;
 	  VARG_NUMBER pri; VARG_CONSTR patcom; VARG_TACTIC tacexp] ->
-           let pat = Pattern.raw_sopattern_of_compattern 
-		       (Global.env()) patcom in
+           let pat =
+	     Astterm.interp_constrpattern Evd.empty (Global.env()) patcom in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function VARG_IDENTIFIER i -> string_of_id i
 		      	 | _ -> bad_vernac_args "HintConstructors") l in
@@ -464,10 +469,10 @@ let fmt_hint_list_for_head c =
       dbs 
   in
   if valid_dbs = [] then 
-    [<'sTR "No hint declared for :"; prterm c >]
+    [<'sTR "No hint declared for :"; pr_ref_label c >]
   else 
     hOV 0 
-      [< 'sTR"For "; prterm c; 'sTR" -> ";
+      [< 'sTR"For "; pr_ref_label c; 'sTR" -> ";
 	 prlist (fun (name,db,hintlist) ->
 	 	   [< 'sTR "  In the database "; 'sTR name; 'sTR " :"; 'fNL;
 		      fmt_hint_list hintlist >])
@@ -475,7 +480,8 @@ let fmt_hint_list_for_head c =
 
 let fmt_hint_id id = 
   try 
-    let c = Declare.global_reference CCI id in fmt_hint_list_for_head c
+    let c = Declare.global_reference CCI id in
+    fmt_hint_list_for_head (head_of_constr_reference c)
   with Not_found -> 
     [< print_id id; 'sTR " not declared" >]
 
@@ -488,16 +494,17 @@ let fmt_hint_term cl =
       | hdc::args -> (hdc,args)
       | [] -> assert false 
     in
+    let hd = head_of_constr_reference hdc in
     let dbs = stringmap_to_list !searchtable in
     let valid_dbs = 
       if occur_existential cl then 
 	map_succeed 
-	  (fun (name, db) -> (name, db, Hint_db.map_all hdc db)) 
+	  (fun (name, db) -> (name, db, Hint_db.map_all hd db)) 
 	  dbs
       else 
 	map_succeed 
 	  (fun (name, db) -> 
-	     (name, db, Hint_db.map_auto (hdc,applist(hdc,args)) db)) 
+	     (name, db, Hint_db.map_auto (hd,applist(hdc,args)) db)) 
 	  dbs
     in 
     if valid_dbs = [] then 
@@ -525,7 +532,7 @@ let print_hint_db db =
   Hint_db.iter 
     (fun head hintlist ->
        mSG (hOV 0 
-	      [< 'sTR "For "; prterm head; 'sTR " -> "; 
+	      [< 'sTR "For "; pr_ref_label head; 'sTR " -> "; 
 		 fmt_hint_list hintlist; 'fNL >]))
     db
 
@@ -644,8 +651,9 @@ and my_find_search db_list local_db hdc concl =
 
 and trivial_resolve db_list local_db cl = 
   try 
+    let hdconstr = List.hd (head_constr_bound cl []) in
     priority 
-      (my_find_search db_list local_db (List.hd (head_constr_bound cl [])) cl)
+      (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
   with Bound | Not_found -> 
     []
 
@@ -685,9 +693,9 @@ let h_trivial = hide_tactic "Trivial" dyn_trivial
 
 let possible_resolve db_list local_db cl =
   try 
+    let hdconstr = List.hd (head_constr_bound cl []) in
     List.map snd 
-      (my_find_search db_list local_db 
-	 (List.hd (head_constr_bound cl [])) cl)
+      (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
   with Bound | Not_found -> 
     []
 
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 82a8ee792f..fce449c027 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -12,17 +12,19 @@ open Clenv
 (*i*)
   
 type auto_tactic = 
-  | Res_pf     of constr * unit clausenv (* Hint Apply *)
-  | ERes_pf    of constr * unit clausenv (* Hint EApply *)
+  | Res_pf     of constr * unit clausenv    (* Hint Apply *)
+  | ERes_pf    of constr * unit clausenv    (* Hint EApply *)
   | Give_exact of constr                  
   | Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *)
-  | Unfold_nth of constr                 (* Hint Unfold *)
-  | Extern     of Coqast.t               (* Hint Extern *)
+  | Unfold_nth of constr                    (* Hint Unfold *)
+  | Extern     of Coqast.t (* Hint Extern *)
+
+open Rawterm
 
 type pri_auto_tactic = { 
   hname : identifier;     (* name of the hint *)
   pri   : int;            (* A number between 0 and 4, 4 = lower priority *)
-  pat   : constr option;  (* A pattern for the concl of the Goal *)
+  pat   : constr_pattern option; (* A pattern for the concl of the Goal *)
   code  : auto_tactic;    (* the tactic to apply when the concl matches pat *)
 }
 
@@ -34,12 +36,12 @@ module Hint_db :
   sig
     type t
     val empty : t
-    val find : constr -> t -> search_entry
-    val map_all : constr -> t -> pri_auto_tactic list
-    val map_auto : constr * constr -> t -> pri_auto_tactic list
-    val add_one : constr * pri_auto_tactic -> t -> t
-    val add_list : (constr * pri_auto_tactic) list -> t -> t
-    val iter : (constr -> stored_data list -> unit) -> t -> unit
+    val find : constr_label -> t -> search_entry
+    val map_all : constr_label -> t -> pri_auto_tactic list
+    val map_auto : constr_label * constr -> t -> pri_auto_tactic list
+    val add_one : constr_label * pri_auto_tactic -> t -> t
+    val add_list : (constr_label * pri_auto_tactic) list -> t -> t
+    val iter : (constr_label -> stored_data list -> unit) -> t -> unit
   end
 
 type frozen_hint_db_table = Hint_db.t Stringmap.t
@@ -54,7 +56,7 @@ val searchtable : hint_db_table
    [ctyp] is the type of [hc]. *)
 
 val make_exact_entry :
-  identifier -> constr * constr -> constr * pri_auto_tactic
+  identifier -> constr * constr -> constr_label * pri_auto_tactic
 
 (* [make_apply_entry (eapply,verbose) name (c,cty)].
    [eapply] is true if this hint will be used only with EApply;
@@ -63,7 +65,8 @@ val make_exact_entry :
    [cty] is the type of [hc]. *)
 
 val make_apply_entry :
-  bool * bool -> identifier -> constr * constr -> constr * pri_auto_tactic
+  bool * bool -> identifier -> constr * constr
+      -> constr_label * pri_auto_tactic
 
 (* A constr which is Hint'ed will be:
    (1) used as an Exact, if it does not start with a product
@@ -74,19 +77,21 @@ val make_apply_entry :
 
 val make_resolves :
   identifier -> bool * bool -> constr * constr -> 
-    (constr * pri_auto_tactic) list
+    (constr_label * pri_auto_tactic) list
 
 (* [make_resolve_hyp hname htyp].
    used to add an hypothesis to the local hint database;
    Never raises an User_exception;
    If the hyp cannot be used as a Hint, the empty list is returned. *)
 
-val make_resolve_hyp : identifier -> constr -> (constr * pri_auto_tactic) list
+val make_resolve_hyp : identifier -> constr
+      -> (constr_label * pri_auto_tactic) list
 
 (* [make_extern name pri pattern tactic_ast] *)
 
 val make_extern :
-  identifier -> int -> constr -> Coqast.t -> constr * pri_auto_tactic
+  identifier -> int -> constr_pattern -> Coqast.t
+      -> constr_label * pri_auto_tactic
 
 (* Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints *)
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index e6a4b43dd8..3dbbacea69 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -3,6 +3,7 @@
 
 open Term
 open Termdn
+open Rawterm
 
 (* Discrimination nets with bounded depth.
    See the module dn.ml for further explanations.
@@ -26,7 +27,7 @@ let bounded_constr_val_discr (t,depth) =
       | None -> None
       | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
 
-type 'a t = (lbl,constr * int,'a) Dn.t
+type 'a t = (constr_label,constr_pattern * int,'a) Dn.t
 
 let create = Dn.create
 
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 882f0bbb9c..2d0b2f1065 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -4,6 +4,7 @@
 (*i*)
 open Generic
 open Term
+open Rawterm
 (*i*)
 
 (* Discrimination nets with bounded depth. *)
@@ -12,10 +13,10 @@ type 'a t
 
 val create : unit -> 'a t
 
-val add : 'a t -> (constr * 'a) -> 'a t
-val rmv : 'a t -> (constr * 'a) -> 'a t
+val add : 'a t -> (constr_pattern * 'a) -> 'a t
+val rmv : 'a t -> (constr_pattern * 'a) -> 'a t
 
-val lookup : 'a t -> constr -> (constr * 'a) list
-val app : ((constr * 'a) -> unit) -> 'a t -> unit
+val lookup : 'a t -> constr -> (constr_pattern * 'a) list
+val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit
 
 val dnet_depth : int ref
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 5969cebbbb..0ca3f6b2a8 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -8,7 +8,7 @@
    The idea here is that we are going to store patterns.  These
    patterns look like:
 
-   TYP=<patern>
+   TYP=<pattern>
    SORT=<pattern>
 
    and from these patterns, we will be able to decide which tactic to
@@ -111,6 +111,7 @@ open Generic
 open Term
 open Environ
 open Reduction
+open Rawterm
 open Proof_trees
 open Tacmach
 open Tactics
@@ -127,8 +128,8 @@ open Pcoq
 
 (* two patterns - one for the type, and one for the type of the type *)
 type destructor_pattern = {
-  d_typ: constr; 
-  d_sort: constr }
+  d_typ: Rawterm.constr_pattern; 
+  d_sort: Rawterm.constr_pattern }
     
 type ('a,'b) location = Hyp of 'a | Concl of 'b
 
@@ -215,16 +216,17 @@ let _ =
 	     | _ -> assert false
 	   in
 	   fun () ->
-	     let pat = raw_sopattern_of_compattern (Global.env()) patcom in
+	     let (_,pat) = Astterm.interp_constrpattern
+			Evd.empty (Global.env()) patcom in
 	     let code = Ast.to_act_check_vars ["$0",ETast] ETast tacexp in
 	     add_destructor_hint na
                (match loc with
 		  | Hyp b ->
-		      Hyp(b,{d_typ=pat;d_sort=DOP0(Meta(new_meta()))},
-			  { d_typ=DOP0(Meta(new_meta()));
-		       	    d_sort=DOP0(Meta(new_meta())) })
+		      Hyp(b,{d_typ=pat;d_sort=PMeta(new_meta())},
+			  { d_typ=PMeta(new_meta());
+		       	    d_sort=PMeta(new_meta()) })
 		  | Concl () ->
-		      Concl({d_typ=pat;d_sort=DOP0(Meta(new_meta()))}))
+		      Concl({d_typ=pat;d_sort=PMeta(new_meta())}))
                pri code
        | _ -> bad_vernac_args "HintDestruct")
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9f207d27da..1880b5a097 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -173,15 +173,16 @@ let find_constructor env sigma c =
     | _ -> error "find_constructor"
 
 type leibniz_eq = {
-  eq   : marked_term;
-  ind  : marked_term;
-  rrec : marked_term option;
-  rect : marked_term option;
-  congr: marked_term;
-  sym  : marked_term }
+  eq   : marked_pattern;
+  ind  : marked_pattern;
+  rrec : marked_pattern option;
+  rect : marked_pattern option;
+  congr: marked_pattern;
+  sym  : marked_pattern }
 
 let mmk = make_module_marker [ "Prelude"; "Logic_Type"; "Specif"; "Logic" ]
 
+(* Patterns *)
 let eq_pattern = put_pat mmk "(eq ? ? ?)"
 let not_pattern = put_pat mmk "(not ?)"
 let imp_False_pattern = put_pat mmk "? -> False"
@@ -1119,12 +1120,12 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
 
  *)
 
+(* squeletons *)
+let comp_carS_squeleton = put_pat mmk "<<x>>(projS1 ? ? (?)@[x])"
+let comp_cdrS_squeleton = put_pat mmk "<<x>>(projS2 ? ? (?)@[x])"
 
-let comp_carS_pattern = put_pat mmk "<<x>>(projS1 ? ? (?)@[x])"
-let comp_cdrS_pattern = put_pat mmk "<<x>>(projS2 ? ? (?)@[x])"
-
-let comp_carT_pattern = put_pat mmk "<<x>>(projT1 ? ? (?)@[x])"
-let comp_cdrT_pattern = put_pat mmk "<<x>>(projT2 ? ? (?)@[x])"
+let comp_carT_squeleton = put_pat mmk "<<x>>(projT1 ? ? (?)@[x])"
+let comp_cdrT_squeleton = put_pat mmk "<<x>>(projT2 ? ? (?)@[x])"
 
 let dest_somatch_sigma ex ex_pat =
   match dest_somatch ex ex_pat with
@@ -1133,11 +1134,11 @@ let dest_somatch_sigma ex ex_pat =
 
 let find_sigma_data_decompose ex =
   try 
-    (comp_carS_pattern, comp_cdrS_pattern,
+    (comp_carS_squeleton, comp_cdrS_squeleton,
      dest_somatch_sigma ex existS_pattern)
   with _ -> 
     (try 
-       (comp_carT_pattern,comp_cdrT_pattern,
+       (comp_carT_squeleton,comp_cdrT_squeleton,
         dest_somatch_sigma ex existT_pattern)   
      with _ -> 
        errorlabstrm "find_sigma_data_decompose" [< >])
@@ -1145,10 +1146,10 @@ let find_sigma_data_decompose ex =
 let decomp_tuple_term env = 
   let rec decomprec to_here_fun ex =
     try
-      let (comp_car_pattern,comp_cdr_pattern,(a,p,car,cdr)) =
+      let (comp_car_squeleton,comp_cdr_squeleton,(a,p,car,cdr)) =
 	find_sigma_data_decompose  ex in
-      let car_code = soinstance comp_car_pattern [a;p;to_here_fun]
-      and cdr_code = soinstance comp_cdr_pattern [a;p;to_here_fun] in
+      let car_code = soinstance comp_car_squeleton [a;p;to_here_fun]
+      and cdr_code = soinstance comp_cdr_squeleton [a;p;to_here_fun] in
       (car,named_hd env a Anonymous,car_code)::(decomprec cdr_code cdr)
     with e when catchable_exception e ->
       [(ex,named_hd env ex Anonymous,to_here_fun)]
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index ec5de39c03..e762531d42 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -20,11 +20,12 @@ open Library
    Eduardo (5/8/97) *)
 
 type ('na,'a) t = {
-  mutable table : ('na,constr * 'a) Gmap.t;
-  mutable patterns : (Termdn.lbl option,'a Btermdn.t) Gmap.t }
+  mutable table : ('na,Rawterm.constr_pattern * 'a) Gmap.t;
+  mutable patterns : (Rawterm.constr_label option,'a Btermdn.t) Gmap.t }
 
 type ('na,'a) frozen_t = 
-    ('na,constr * 'a) Gmap.t * (Termdn.lbl option,'a Btermdn.t) Gmap.t
+    ('na,Rawterm.constr_pattern * 'a) Gmap.t
+    * (Rawterm.constr_label option,'a Btermdn.t) Gmap.t
 
 let create () =
   { table = Gmap.empty;
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index e94a21e9d5..5275805236 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -4,6 +4,7 @@
 (*i*)
 open Generic
 open Term
+open Rawterm
 (*i*)
 
 (* Named, bounded-depth, term-discrimination nets. *)
@@ -13,18 +14,18 @@ type ('na,'a) frozen_t
 
 val create : unit -> ('na,'a) t
 
-val add : ('na,'a) t -> ('na * (constr * 'a)) -> unit
+val add : ('na,'a) t -> ('na * (constr_pattern * 'a)) -> unit
 val rmv : ('na,'a) t -> 'na -> unit
 val in_dn : ('na,'a) t -> 'na -> bool
-val remap : ('na,'a) t -> 'na -> (constr * 'a) -> unit
+val remap : ('na,'a) t -> 'na -> (constr_pattern * 'a) -> unit
 
-val lookup : ('na,'a) t -> constr -> (constr * 'a) list
-val app : ('na -> (constr * 'a) -> unit) -> ('na,'a) t -> unit
+val lookup : ('na,'a) t -> constr -> (constr_pattern * 'a) list
+val app : ('na -> (constr_pattern * 'a) -> unit) -> ('na,'a) t -> unit
 
 val dnet_depth : int ref
 
 val freeze : ('na,'a) t -> ('na,'a) frozen_t
 val unfreeze : ('na,'a) frozen_t -> ('na,'a) t -> unit
 val empty : ('na,'a) t -> unit
-val to2lists : ('na,'a) t -> ('na * (Term.constr * 'a)) list * 
-                             (Termdn.lbl option * 'a Btermdn.t) list
+val to2lists : ('na,'a) t -> ('na * (Rawterm.constr_pattern * 'a)) list * 
+                             (Rawterm.constr_label option * 'a Btermdn.t) list
diff --git a/tactics/pattern.ml b/tactics/pattern.ml
index 23b6da6e46..19d0207294 100644
--- a/tactics/pattern.ml
+++ b/tactics/pattern.ml
@@ -12,6 +12,7 @@ open Environ
 open Proof_trees
 open Stock
 open Clenv
+open Rawterm
 
 (* The pattern table for tactics. *)
 
@@ -21,33 +22,38 @@ open Clenv
 
 type module_mark = Stock.module_mark
 
-type marked_term = constr Stock.stocked
-
-let rec whd_replmeta = function
-  | DOP0(XTRA("ISEVAR")) -> DOP0(Meta (new_meta()))
-  | DOP2(Cast,c,_) -> whd_replmeta c
-  | c -> c
-
-let raw_sopattern_of_compattern env com =
-  let c = Astterm.constr_of_com_pattern Evd.empty env com in
-  strong (fun _ _ -> whd_replmeta) env Evd.empty c
+let parse_constr s =
+  try 
+    Pcoq.parse_string Pcoq.Constr.constr_eoi s 
+  with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
+    error "Syntax error : not a construction" 
 
+(* Patterns *)
 let parse_pattern s =
-  let com =
-    try 
-      Pcoq.parse_string Pcoq.Constr.constr_eoi s 
-    with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
-      error "Malformed pattern" 
-  in
-  raw_sopattern_of_compattern (Global.env()) com
+  Astterm.interp_constrpattern Evd.empty (Global.env()) (parse_constr s)
     
-let (pattern_stock : constr Stock.stock) =
+type marked_pattern = (int list * constr_pattern) Stock.stocked
+
+let (pattern_stock : (int list * constr_pattern) Stock.stock) =
   Stock.make_stock { name = "PATTERN"; proc = parse_pattern }
 
-let make_module_marker = Stock.make_module_marker pattern_stock
 let put_pat = Stock.stock pattern_stock
 let get_pat = Stock.retrieve pattern_stock
 
+let make_module_marker = Stock.make_module_marker
+
+(* Squeletons *)
+let parse_squeleton s =
+  Astterm.interp_constr Evd.empty (Global.env()) (parse_constr s)
+
+type marked_term = constr Stock.stocked
+
+let (squeleton_stock : constr Stock.stock) =
+  Stock.make_stock { name = "SQUELETON"; proc = parse_squeleton }
+
+let put_squel = Stock.stock squeleton_stock
+let get_squel = Stock.retrieve squeleton_stock
+
 (* Second part : Given a term with second-order variables in it,
    represented by Meta's, and possibly applied using XTRA[$SOAPP] to
    terms, this function will perform second-order, binding-preserving,
@@ -103,7 +109,73 @@ let memb_metavars m n =
   match (m,n) with
     | (None, _)     -> true
     | (Some mvs, n) -> List.mem n mvs
-	  
+
+exception PatternMatchingFailure
+
+let somatch metavars = 
+  let rec sorec stk sigma p t =
+    let cT = whd_castapp t in
+    match p,kind_of_term cT with
+      | PSoApp (n,relargs),m ->
+          assert (memb_metavars metavars n);
+	  let frels = Intset.elements (free_rels cT) in
+	  if list_subset frels relargs then
+	    constrain (n,build_dlam relargs stk cT) sigma
+	  else
+	    raise PatternMatchingFailure
+
+      | PMeta n, m ->
+	  if not (memb_metavars metavars n) then
+	  (*Ce cas est bizarre : comment les numéros pourraient-ils coincider*)
+	    match m with
+	      | IsMeta m0 when n=m0 -> sigma
+	      | _ -> raise PatternMatchingFailure
+	  else
+	    let depth = List.length stk in
+	    let frels = Intset.elements (free_rels cT) in
+            if List.for_all (fun i -> i > depth) frels then
+	      constrain (n,lift (-depth) cT) sigma
+            else 
+	      raise PatternMatchingFailure
+
+      | PRef (RVar v1), IsVar v2 when v1 = v2 -> sigma
+
+      | PRef (RConst (sp1,ctxt1)), IsConst (sp2,ctxt2) 
+	  when sp1 = sp2 && Array.length ctxt1 = Array.length ctxt2 ->
+	  array_fold_left2 (sorec stk) sigma ctxt1 ctxt2
+
+      | PRef (RInd (sp1,ctxt1)), IsMutInd (sp2,ctxt2) 
+	  when sp1 = sp2 && Array.length ctxt1 = Array.length ctxt2 ->
+	  array_fold_left2 (sorec stk) sigma ctxt1 ctxt2
+
+      | PRef (RConstruct (sp1,ctxt1)), IsMutConstruct (sp2,ctxt2) 
+	  when sp1 = sp2 && Array.length ctxt1 = Array.length ctxt2 ->
+	  array_fold_left2 (sorec stk) sigma ctxt1 ctxt2
+
+      | PRel n1, IsRel n2 when n1 = n2 -> sigma
+
+      | PSort (RProp c1), IsSort (Prop c2) when c1 = c2 -> sigma
+
+      | PSort RType, IsSort (Type _) -> sigma
+
+      | PApp (c1,arg1), IsAppL (c2,arg2) ->
+	  array_fold_left2 (sorec stk) (sorec stk sigma c1 c2)
+	    arg1 (Array.of_list arg2)
+
+      | PBinder(BProd,na1,c1,d1), IsProd(na2,c2,d2) ->
+	  sorec (na2::stk) (sorec stk sigma c1 c2) d1 d2
+
+      | PBinder(BLambda,na1,c1,d1), IsLambda(na2,c2,d2) ->
+	  sorec (na2::stk) (sorec stk sigma c1 c2) d1 d2
+
+      | _, (IsFix _ | IsMutCase _ | IsCoFix _) ->
+	  error "somatch: not implemented"
+
+      | _ -> raise PatternMatchingFailure
+
+    in 
+    sorec [] []
+(*
 let somatch metavars = 
   let rec sorec stk sigma p t =
     let cP = whd_castapp p 
@@ -175,26 +247,27 @@ let somatch metavars =
   	    | _ -> error "somatch"
     in 
     sorec [] []
-
+*)
 let somatches n pat =
-  let m = get_pat pat in 
+  let (_,m) = get_pat pat in 
   try 
     let _ = somatch None m n in true 
   with e when Logic.catchable_exception e -> 
     false
 
 let dest_somatch n pat =
-  let m = get_pat pat in
-  let mvs = collect_metas m in
+  let mvs,m = get_pat pat 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 mvs = collect_metas m in
+let newsomatch n pat = let _,m = get_pat pat in somatch None m n
+
+let soinstance squel arglist =
+  let c = get_squel squel in
+  let mvs = collect_metas c in
   let mvb = List.combine mvs arglist in 
   Sosub.soexecute (Reduction.strong (fun _ _ -> Reduction.whd_meta mvb) 
-		     empty_env Evd.empty m)
+		     empty_env Evd.empty c)
 
 (* I implemented the following functions which test whether a term t
    is an inductive but non-recursive type, a general conjuction, a
@@ -300,18 +373,18 @@ let is_unit_type t = op2bool (match_with_unit_type t)
    inductive binary relation R, so that R has only one constructor
    stablishing its reflexivity.  *)
 
+let refl_rel_pat1 = put_pat mmk "(A : ?)(x:A)(? A x x)"
+let refl_rel_pat2 = put_pat mmk "(x : ?)(? x x)"
+
 let match_with_equation  t =
   let (hdapp,args) = decomp_app t in
   match (kind_of_term hdapp) with
     | IsMutInd ind -> 
-        let constr_types = 
-	  Global.mind_lc_without_abstractions ind 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 constr_types = Global.mind_lc_without_abstractions ind in 
         let nconstr = Global.mind_nconstr ind in
 	if nconstr = 1 &&
-           (somatches constr_types.(0) refl_rel_term1 ||
-            somatches constr_types.(0) refl_rel_term2) 
+           (somatches constr_types.(0) refl_rel_pat1 ||
+            somatches constr_types.(0) refl_rel_pat2) 
         then 
 	  Some (hdapp,args)
         else 
@@ -335,3 +408,31 @@ let is_nottype t = op2bool (match_with_nottype t)
 let is_imp_term = function
   | DOP2(Prod,_,DLAM(_,b)) -> not (dependent (Rel 1) b)
   | _                      -> false
+
+let rec pattern_of_constr t =
+  match kind_of_term t with
+    | IsRel n  -> PRel n
+    | IsMeta n -> PMeta n
+    | IsVar id -> PRef (RVar id)
+    | IsSort (Prop c) -> PSort (RProp c)
+    | IsSort (Type _) -> PSort RType
+    | IsCast (c,t)      -> pattern_of_constr c
+    | IsProd (na,c,b)   ->
+	PBinder (BProd,na,pattern_of_constr c,pattern_of_constr b)
+    | IsLambda (na,c,b) ->
+	PBinder (BLambda,na,pattern_of_constr c,pattern_of_constr b)
+    | IsAppL (f,args)   ->
+	PApp (pattern_of_constr f,
+	      Array.of_list (List.map pattern_of_constr args))
+    | IsConst (cst_sp,ctxt)         ->
+	PRef (RConst (cst_sp,Array.map pattern_of_constr ctxt))
+    | IsMutInd (ind_sp,ctxt)        ->
+	PRef (RInd (ind_sp,Array.map pattern_of_constr ctxt))
+    | IsMutConstruct (cstr_sp,ctxt) ->
+	PRef (RConstruct (cstr_sp,Array.map pattern_of_constr ctxt))
+    | IsMutCase _ | IsFix _ | IsCoFix _ ->
+	error "pattern_of_constr: destructors currently not supported"
+    | IsEvar _ -> error "pattern_of_constr: an existential variable remains"
+    | IsAbst _ | IsXtra _   -> anomaly "No longer supported"
+
+
diff --git a/tactics/pattern.mli b/tactics/pattern.mli
index afe1ec848e..ae59ddef31 100644
--- a/tactics/pattern.mli
+++ b/tactics/pattern.mli
@@ -37,17 +37,43 @@ open Proof_trees
    at tactic-application time.  The ONLY difference will be that
    no implicit syntax resolution will happen. *)
 
-(*s First part : introduction of term patterns *)
+(* A pattern is intented to be pattern-matched (using functions
+   [somatch] and co), while a squeleton is a term with holes intented to
+   be substituted by [soinstance] *)
 
-type module_mark = Stock.module_mark
-type marked_term
+(*s First part : introduction of term patterns and term squeletons *)
 
+(* [make_module_marker modl] makes a key from the list of
+   vernacular modules [modl] where names in a pattern or squeleton has
+   to be searched *)
+
+type module_mark = Stock.module_mark
 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
 
+(* [put_pat mmk s] declares a pattern [s] to be parsed using the
+   definitions in the modules associated to the key [mmk] *)
+
+type marked_pattern
+val put_pat            : module_mark -> string -> marked_pattern
+(*val get_pat            : marked_pattern -> constr*)
+
+
+(* [pattern_of_constr c] translates a term [c] with metavariables into
+   a pattern; currently, no destructor (Cases, Fix, Cofix) and no
+   existential variable are allowed in [c] *)
+
+val pattern_of_constr : constr -> Rawterm.constr_pattern
+
+(* [put_squel mmk s] declares an open term [s] to be parsed using the
+   definitions in the modules associated to the key [mmk] *)
+
+type marked_term
+val put_squel          : module_mark -> string -> marked_term
+(*val get_squel          : marked_term -> constr*)
+
+(*i Remplacé par Astterm.interp_constrpattern
 val raw_sopattern_of_compattern : Environ.env -> 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
@@ -69,9 +95,12 @@ val raw_sopattern_of_compattern : Environ.env -> 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      : int list option -> constr -> constr -> (int * constr) list
-val somatches    : constr -> marked_term -> bool
-val dest_somatch : constr -> marked_term -> constr list
+(*i Devrait être une fonction de filtrage externe i*)
+val somatch      : int list option -> Rawterm.constr_pattern -> constr -> (int * constr) list
+
+val somatches    : constr -> marked_pattern -> bool
+val dest_somatch : constr -> marked_pattern -> constr list
+
 val soinstance   : marked_term -> constr list -> constr 
 
 val is_imp_term : constr -> bool
diff --git a/tactics/stock.ml b/tactics/stock.ml
index b0fa6d0e81..ef0feec952 100644
--- a/tactics/stock.ml
+++ b/tactics/stock.ml
@@ -59,7 +59,7 @@ let mmk_ctr = ref 0
 
 let new_mmk () = (incr mmk_ctr; !mmk_ctr)
 
-let make_module_marker stock sl =
+let make_module_marker sl =
   let sorted_sl = Sort.list (<) sl in 
   try 
     Bij.map !path_mark_bij sorted_sl
diff --git a/tactics/stock.mli b/tactics/stock.mli
index bbc9195147..c0cd43c7d5 100644
--- a/tactics/stock.mli
+++ b/tactics/stock.mli
@@ -18,7 +18,7 @@ type 'a stock_args = {
   proc : string -> 'a }
 
 val make_stock : 'a stock_args -> 'a stock
-val make_module_marker : 'a stock -> string list -> module_mark
+val make_module_marker : string list -> module_mark
 val stock : 'a stock -> module_mark -> string -> 'a stocked
 val retrieve : 'a stock -> 'a stocked -> 'a
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 54d04def05..baae41399b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -118,16 +118,14 @@ let clause_type cls gl =
 
 (* Functions concerning matching of clausal environments *)
 
-let matches gls n pat =
-  let m = get_pat pat in
+let matches gls n m =
   let (wc,_) = startWalk gls in 
   try 
     let _ = Clenv.unify_0 [] wc m n in true 
   with e when Logic.catchable_exception e -> 
     false
 
-let dest_match gls n pat =
-  let m       = get_pat pat in
+let dest_match gls n m =
   let mvs     = collect_metas m in
   let (wc,_)  = startWalk gls in
   let (mvb,_) = Clenv.unify_0 [] wc m n in 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 7884ba02eb..e7d8cff25e 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -48,8 +48,13 @@ val tclTHEN_i1     : tactic -> (int -> tactic) -> tactic
 val nth_clause  : int -> goal sigma -> clause
 val clause_type : clause -> goal sigma -> constr
 
+(*
 val matches      : goal sigma -> constr -> marked_term -> bool
 val dest_match   : goal sigma -> constr -> marked_term -> constr list
+*)
+(* The second argument is the pattern *)
+val matches      : goal sigma -> constr -> constr -> bool
+val dest_match   : goal sigma -> constr -> constr -> constr list
 
 val allHyps    : goal sigma -> clause list
 val afterHyp   : identifier -> goal sigma -> clause list
@@ -78,7 +83,7 @@ val ifOnClause     :
    [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the
    right values to build a tactic *)
 
-val conclPattern : constr -> constr -> Coqast.t -> tactic
+val conclPattern : constr -> Rawterm.constr_pattern -> Coqast.t -> tactic
 
 (*s Elimination tacticals. *)
 
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 4fcfc0264e..334eb304ec 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -46,6 +46,7 @@ let classically cltac = function
 
 let somatch m pat = somatch None (get_pat pat) m
 let module_mark   = ["Logic"]
+(* patterns *)
 let mmk           = make_module_marker ["Prelude"]
 let false_pattern = put_pat mmk "False"
 let true_pattern = put_pat mmk "True"
@@ -54,9 +55,12 @@ let or_pattern    = put_pat mmk "(or ? ?)"
 let eq_pattern    = put_pat mmk "(eq ? ? ?)"
 let pi_pattern    = put_pat mmk "(x : ?)((?)@[x])"
 let imply_pattern = put_pat mmk "?1 -> ?2"
+let atomic_imply_bot_pattern = put_pat mmk "?1 -> ?2"
 let iff_pattern   = put_pat mmk "(iff ? ?)"
 let not_pattern   = put_pat mmk "(not ?1)"
-let mkIMP a b     = soinstance imply_pattern [a;b]    
+(* squeletons *)
+let imply_squeleton = put_pat mmk "?1 -> ?2"
+let mkIMP a b       = soinstance imply_squeleton [a;b]    
 
 let is_atomic m =
  (not (is_conjunction m)     ||
@@ -120,7 +124,6 @@ let dyck_imply_intro = (dImp None)
     --------------
     A->B,A,Gamma |- G  (A Atomique)
  *)
-let atomic_imply_bot_pattern = put_pat mmk "?1 -> ?2"
 
 let atomic_imply_step cls gls =
   let mvb = somatch (clause_type cls gls) atomic_imply_bot_pattern in 
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index fda033f268..957543e16d 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -3,18 +3,15 @@
 
 open Util
 open Generic
+open Names
 open Term
+open Rawterm
 
 (* Discrimination nets of terms.
    See the module dn.ml for further explanations.
    Eduardo (5/8/97) *)
 
-type lbl =
-  | TERM of constr
-  | DOPER of sorts oper
-  | DLAMBDA
-
-type 'a t = (lbl,constr,'a) Dn.t
+type 'a t = (constr_label,constr_pattern,'a) Dn.t
 
 (*If we have: f a b c ..., decomp gives: (f,[a;b;c;...])*)
 
@@ -24,26 +21,31 @@ let decomp =
     | DOP2(Cast,c1,_) -> decrec acc c1
     | c -> (c,acc)
   in 
-  decrec []   
+  decrec []
 
+let decomp_pat = 
+  let rec decrec acc = function
+    | PApp (f,args) -> decrec (Array.to_list args @ acc) f
+    | c -> (c,acc)
+  in 
+  decrec []   
 
 let constr_pat_discr t =
-  if not(occur_meta t) then 
+  if not (occur_meta_pattern t) then 
     None
   else
-    match decomp t with
-      (* | DOPN(Const _,_) as c,l -> Some(TERM c,l) *)
-      | DOPN(MutInd _,_) as c,l -> Some(TERM c,l)
-      | DOPN(MutConstruct _,_) as c,l -> Some(TERM c,l)
-      | VAR _ as c,l -> Some(TERM c,l)
-      | c -> None
+    match decomp_pat t with
+      | PRef (RInd (ind_sp,_)), args -> Some(IndNode ind_sp,args)
+      | PRef (RConstruct (cstr_sp,_)), args -> Some(CstrNode cstr_sp,args)
+      | PRef (RVar id), args -> Some(VarNode id,args)
+      | _ -> None
 
 let constr_val_discr t =
   match decomp t with
     (* DOPN(Const _,_) as c,l -> Some(TERM c,l) *)
-    | DOPN(MutInd _,_) as c,l -> Some(TERM c,l)
-    | DOPN(MutConstruct _,_) as c,l -> Some(TERM c,l)
-    | VAR _ as c,l -> Some(TERM c,l)
+    | DOPN(MutInd ind_sp,_) as c,l -> Some(IndNode ind_sp,l)
+    | DOPN(MutConstruct cstr_sp,_) as c,l -> Some(CstrNode cstr_sp,l)
+    | VAR id as c,l -> Some(VarNode id,l)
     | c -> None
 
 (* Les deux fonctions suivantes ecrasaient les precedentes, 
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index 62066f604e..1b8a132abf 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -4,6 +4,7 @@
 (*i*)
 open Generic
 open Term
+open Rawterm
 (*i*)
   
 (* Discrimination nets of terms. *)
@@ -22,26 +23,23 @@ val create : unit -> 'a t
 
 (* [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *)
 
-val add : 'a t -> (constr * 'a) -> 'a t
+val add : 'a t -> (constr_pattern * 'a) -> 'a t
 
-val rmv : 'a t -> (constr * 'a) -> 'a t
+val rmv : 'a t -> (constr_pattern * 'a) -> 'a t
 
 (* [lookup t c] looks for patterns (with their action) matching term [c] *)
 
-val lookup : 'a t -> constr -> (constr * 'a) list
+val lookup : 'a t -> constr -> (constr_pattern * 'a) list
 
-val app : ((constr * 'a) -> unit) -> 'a t -> unit
+val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit
 
 
 (*i*)
 (* These are for Nbtermdn *)
 
-type lbl =
-  | TERM of constr
-  | DOPER of sorts oper
-  | DLAMBDA
-
-val constr_pat_discr : constr -> (lbl * constr list) option
-val constr_val_discr : constr -> (lbl * constr list) option
+val constr_pat_discr : 
+  constr_pattern -> (constr_label * constr_pattern list) option
+val constr_val_discr :
+  constr -> (constr_label * constr list) option
 
 (*i*)