Déplacement du type reference dans Term

Découpage de tactics/pattern en proofs/pattern et tactics/hipattern
Renommage des fonctions somatch and co dans Pattern et Tacticals
Divers extensions pour utiliser les constr_pattern


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

16 files changed, 261 insertions, 163 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 3ed337847d..bd14984538 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -547,16 +547,30 @@ let destUntypedCoFix = function
       (i,types,funnames,bodies)
   | _ -> invalid_arg "destCoFix"
 
+(**********************************************************************)
 
-(******************)
-(* Term analysis  *)
-(******************)
+type binder_kind = BProd | BLambda
+
+type fix_kind = RFix of int array * int | RCofix of int
+
+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 * 'ctxt
+  | RMeta of int
 
 type existential = int * constr array
 type constant = section_path * constr array
 type constructor = constructor_path * constr array
 type inductive = inductive_path * constr array
 
+(******************)
+(* Term analysis  *)
+(******************)
+
 type kindOfTerm = 
   | IsRel          of int
   | IsMeta         of int
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index dd2f1b5d8b..a096c833a0 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -12,6 +12,7 @@ open Evd
 open Reduction
 open Impargs
 open Rawterm
+open Pattern
 open Typing
 open Pretyping
 open Evarutil
@@ -569,7 +570,7 @@ let rec pat_of_ref metas vars = function
   | RInd (ip,ctxt) -> RInd (ip, ctxt)
   | RConstruct(cp,ctxt) ->RConstruct(cp, ctxt)
   | REVar (n,ctxt) -> REVar (n, ctxt)
-  | RMeta n -> RMeta n
+  | RMeta n -> metas := n::!metas; RMeta n
   | RAbst _ -> error "pattern_of_rawconstr: not implemented"
   | RVar _ -> assert false (* Capturé dans pattern_of_raw *)
 
@@ -587,11 +588,8 @@ and pat_of_raw metas vars = function
 	       pat_of_raw metas (na::vars) c2)
   | RSort (_,s) ->
       PSort s
-  | RHole _ -> error "Place-holders must be numbered in patterns"
-(*
-      let n = new_meta () in
-      metas := n::!metas;
-      PMeta n *)
+  | RHole _ ->
+      PMeta None
   | RCast (_,c,t) ->
       warning "Cast not taken into account in constr pattern";
       pat_of_raw metas vars c
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 10e43172b7..19773d6869 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -47,15 +47,22 @@ let print_typed_value_in_env env (trm,typ) =
      'sTR "     : "; prterm_env (gLOB sign) typ ; 'fNL >]
 
 let print_typed_value x = print_typed_value_in_env (Global.env ()) x
+
+let pkprinters = function
+  | FW -> (fprterm,fprterm_env)
+  | CCI -> (prterm,prterm_env)
+  | _ -> anomaly "pkprinters"
 			  		  
 let print_recipe = function
   | Some { contents = Cooked c } -> prterm c
   | Some { contents = Recipe _ } -> [< 'sTR"<recipe>" >]
   | None -> [< 'sTR"<uncookable>" >]
 
+(*
 let fprint_recipe = function
   | Some c -> fprterm c
   | None -> [< 'sTR"<uncookable>" >]
+*)
 
 let print_typed_recipe (val_0,typ) =
   [< print_recipe val_0; 'fNL; 'sTR "     : "; prtype typ; 'fNL >]
@@ -77,7 +84,7 @@ let print_var name typ =
   [< 'sTR "*** [" ; 'sTR name ; 'sTR " : "; prtype typ; 'sTR "]"; 'fNL >]
 
 let print_env pk = 
-  let pterminenv = if pk = FW then fprterm_env else prterm_env in
+  let pterminenv = (* if pk = FW then fprterm_env else *) prterm_env in
   let pr_binder env (na,c) =
     match na with
       | Name id as name ->
@@ -99,8 +106,7 @@ let assumptions_for_print lna =
     (ENVIRON(nil_sign,nil_dbsign))
 
 let print_constructors_with_sep pk fsep mip = 
-  let pterm,pterminenv =
-    if pk = FW then (fprterm,fprterm_env) else (prterm,prterm_env) in
+  let pterm,pterminenv = pkprinters pk in
   let (lna,lC) = decomp_all_DLAMV_name mip.mind_lc in
   let ass_name = assumptions_for_print lna in
   let lidC = Array.to_list 
@@ -131,8 +137,7 @@ let implicit_args_msg sp mipv =
 
 let print_mutual sp mib = 
   let pk = kind_of_path sp in
-  let pterm,pterminenv =
-    if pk = FW then (fprterm,fprterm_env) else (prterm,prterm_env) in
+  let pterm,pterminenv = pkprinters pk in
   let env = Global.env () in
   let evd = Evd.empty in
   let {mind_packets=mipv; mind_nparams=nparams} = mib in 
@@ -271,7 +276,7 @@ let print_leaf_entry with_values sep (sp,lobj) =
       	   print_id id ; 'sTR sep;  
            if with_values then 
              let c = Syntax_def.search_syntactic_definition id in 
-	     [< prrawterm c >]
+	     [< pr_rawterm c >]
            else [<>]; 'fNL >]
     | (_,"PPSYNTAX") -> 
 	[< 'sTR" Syntax Marker"; 'fNL >]
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 36f8d11a36..3e286462e8 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -26,7 +26,7 @@ let pr_global k oper =
   [< 'sTR (string_of_id id) >]
 *)
 
-let globpr k gt = match gt with
+let globpr gt = match gt with
   | Nvar(_,s) -> [< 'sTR s >]
 (*
   | Node(_,"EVAR", (Num (_,ev))::_) ->
@@ -63,62 +63,64 @@ let tactic_syntax_universe = "tactic"
 let constr_initial_prec = Some ((constr_syntax_universe,(9,0,0)),Extend.L)
 let tactic_initial_prec = Some ((tactic_syntax_universe,(9,0,0)),Extend.L)
 
-let gencompr k gt =
-  let uni = match k with
-    | CCI | FW -> constr_syntax_universe
-    | _ -> anomaly "gencompr: not a construction"
-	(* WAS "<undefined>" *)
-  in Esyntax.genprint (globpr k) uni constr_initial_prec gt
+let gentermpr_fail gt =
+  Esyntax.genprint globpr constr_syntax_universe constr_initial_prec gt
 
-(* [at_top] means ids of env must be avoided in bound variables *)
-let gentermpr_core at_top k env t =
-  let uenv = unitize_env env in
-  try gencompr k (Termast.bdize at_top uenv t)
+let gentermpr gt =
+  try gentermpr_fail gt
   with s -> wrap_exception s
 
-let gentermpr k = gentermpr_core false k
-let gentermpr_at_top k = gentermpr_core true k
+(* [at_top] means ids of env must be avoided in bound variables *)
+let gentermpr_core at_top env t =
+  gentermpr (Termast.ast_of_constr at_top (unitize_env env) t)
 
-let prterm_env_at_top a = gentermpr_core true CCI a
-let prterm_env a = gentermpr CCI a
+let prterm_env_at_top env = gentermpr_core true env
+let prterm_env env = gentermpr_core false env
 let prterm = prterm_env (gLOB nil_sign)
 
-let fprterm_env a = gentermpr FW a
-let fprterm = fprterm_env (gLOB nil_sign)
-
 let prtype_env env typ = prterm_env env (incast_type typ)
 let prtype = prtype_env (gLOB nil_sign)
 
+(* Plus de "k"...
+let gentermpr k = gentermpr_core false
+let gentermpr_at_top k = gentermpr_core true
+
+let fprterm_env a = gentermpr FW a
+let fprterm = fprterm_env (gLOB nil_sign)
+
 let fprtype_env env typ = fprterm_env env (incast_type typ)
 let fprtype = fprtype_env (gLOB nil_sign)
+*)
+
+let fprterm_env a = failwith "Fw printing not implemented"
+let fprterm = failwith "Fw printing not implemented"
 
-let pr_constant cst = gencompr CCI (ast_of_constant cst)
-let pr_existential ev = gencompr CCI (ast_of_existential ev)
-let pr_inductive ind = gencompr CCI (ast_of_inductive ind)
-let pr_constructor cstr = gencompr CCI (ast_of_constructor cstr)
+let fprtype_env env typ = failwith "Fw printing not implemented"
+let fprtype = failwith "Fw printing not implemented"
 
-open Rawterm
+(* For compatibility *)
+let fterm0 = fprterm_env
+
+let pr_constant cst = gentermpr (ast_of_constant cst)
+let pr_existential ev = gentermpr (ast_of_existential ev)
+let pr_inductive ind = gentermpr (ast_of_inductive ind)
+let pr_constructor cstr = gentermpr (ast_of_constructor cstr)
+
+open Pattern
 let pr_ref_label = function (* On triche sur le contexte *)
   | ConstNode sp -> pr_constant (sp,[||])
   | IndNode sp -> pr_inductive (sp,[||])
   | CstrNode sp -> pr_constructor (sp,[||])
   | VarNode id -> print_id id
 
+let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t)
+let pr_rawterm t = gentermpr (Termast.ast_of_rawconstr t)
+let pr_pattern_env env t =
+  gentermpr (Termast.ast_of_pattern (unitize_env env) t)
+let pr_pattern t = pr_pattern_env (gLOB nil_sign) t
+
 (* For compatibility *)
 let term0 = prterm_env
-let fterm0 = fprterm_env
-
-let genpatternpr k t =
-  try gencompr k (Termast.ast_of_pattern t)
-  with s -> wrap_exception s
-
-let prpattern = genpatternpr CCI
-
-let genrawtermpr k env t =
-  try gencompr k (Termast.ast_of_rawconstr t)
-  with s -> wrap_exception s
-
-let prrawterm = genrawtermpr CCI (gLOB nil_sign)
 
 let rec gentacpr gt =
   Esyntax.genprint default_tacpr tactic_syntax_universe tactic_initial_prec gt
@@ -130,12 +132,12 @@ and default_tacpr = function
 	[< 'sTR s; 'bRK(1,2); hOV 0 (prlist_with_sep pr_spc gentacpr ta) >]
     | gt -> dfltpr gt
 
-let print_decl k sign (s,typ) =
-  let ptyp = gentermpr k (gLOB sign) (body_of_type typ) in
+let print_decl sign (s,typ) =
+  let ptyp = prterm_env (gLOB sign) (body_of_type typ) in
   [< print_id s ; 'sTR" : "; ptyp >]
 
-let print_binding k env (na,typ) =
-  let ptyp = gentermpr k env (body_of_type typ) in
+let print_binding env (na,typ) =
+  let ptyp = prterm_env env (body_of_type typ) in
   match na with
     | Anonymous -> [< 'sTR"<>" ; 'sTR" : " ; ptyp >]
     | Name id -> [< print_id id ; 'sTR" : "; ptyp >]
@@ -164,34 +166,34 @@ let dbenv_it_with f env e =
 (* Prints a signature, all declarations on the same line if possible *)
 let pr_sign sign =
   hV 0 [< (sign_it_with (fun id t sign pps ->
-                           [< pps; 'wS 2; print_decl CCI sign (id,t) >])
+                           [< pps; 'wS 2; print_decl sign (id,t) >])
              sign) [< >] >]
 
 (* Prints an env (variables and de Bruijn). Separator: newline *)
-let pr_env k env =
+let pr_env env =
   let sign_env =
     sign_it_with
       (fun id t sign pps ->
-         let pidt =  print_decl k sign (id,t) in [< pps; 'fNL; pidt >])
+         let pidt =  print_decl sign (id,t) in [< pps; 'fNL; pidt >])
       (get_globals env) [< >] 
   in
   let db_env =
     dbenv_it_with 
       (fun na t env pps ->
-         let pnat = print_binding k env (na,t) in [< pps; 'fNL; pnat >])
+         let pnat = print_binding env (na,t) in [< pps; 'fNL; pnat >])
       env [< >]
   in 
   [< sign_env; db_env >]
 
 let pr_ne_env header k = function
   | ENVIRON (sign,_) as env when isnull_sign sign & isnull_rel_env env -> [< >]
-  | env -> let penv = pr_env k env in [< header; penv >]
+  | env -> let penv = pr_env env in [< header; penv >]
 
 let pr_env_limit n env =
   let sign = get_globals env in
   let lgsign = sign_length sign in
   if n >= lgsign then 
-    pr_env CCI env
+    pr_env env
   else
     let k = lgsign-n in
     let sign_env =
@@ -200,7 +202,7 @@ let pr_env_limit n env =
            if i < k then 
 	     [< pps ;'sTR "." >] 
 	   else
-             let pidt = print_decl CCI sign (id,t) in
+             let pidt = print_decl sign (id,t) in
 	     [< pps ; 'fNL ;
 		'sTR (emacs_str (String.make 1 (Char.chr 253)));
 		pidt >])
@@ -209,7 +211,7 @@ let pr_env_limit n env =
     let db_env =
       dbenv_it_with
         (fun na t env pps ->
-           let pnat = print_binding CCI env (na,t) in
+           let pnat = print_binding env (na,t) in
 	   [< pps; 'fNL;
 	      'sTR (emacs_str (String.make 1 (Char.chr 253)));
 	      pnat >])
@@ -218,5 +220,5 @@ let pr_env_limit n env =
     [< sign_env; db_env >]
 
 let pr_env_opt env = match Options.print_hyps_limit () with 
-  | None -> hV 0 (pr_env CCI env)
+  | None -> hV 0 (pr_env env)
   | Some n -> hV 0 (pr_env_limit n env)
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 3587ba01e5..dda005f8bb 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -14,6 +14,7 @@ open Impargs
 open Coqast
 open Ast
 open Rawterm
+open Pattern
 
 (* In this file, we translate rawconstr to ast, in order to print constr *)
 
@@ -130,24 +131,24 @@ let ast_of_ref = function
 	    ::(List.map ast_of_ident (* on triche *) []))
   | RInd (ind,ctxt) -> ast_of_inductive_ref (ind,ids_of_ctxt ctxt)
   | RConstruct (cstr,ctxt) -> ast_of_constructor_ref (cstr,ids_of_ctxt ctxt)
-  | RVar id -> nvar (string_of_id id)
+  | RVar id -> ast_of_ident id
   | REVar (ev,ctxt) -> ast_of_existential_ref (ev,ids_of_ctxt ctxt)
   | RMeta n -> ope("META",[num n])
 
 (**********************************************************************)
 (* conversion of patterns                                             *)
 
-let rec ast_of_pattern = function   (* loc is thrown away for printing *)
+let rec ast_of_cases_pattern = function   (* loc is thrown away for printing *)
   | PatVar (loc,Name id) -> nvar (string_of_id id)
   | PatVar (loc,Anonymous) -> nvar "_"
   | PatCstr(loc,cstr,args,Name id) ->
+      let args = List.map ast_of_cases_pattern args in
       ope("PATTAS",
 	  [nvar (string_of_id id);
-	   ope("PATTCONSTRUCT",
-	       (ast_of_constructor_ref cstr)::List.map ast_of_pattern args)])
+	   ope("PATTCONSTRUCT", (ast_of_constructor_ref cstr)::args)])
   | PatCstr(loc,cstr,args,Anonymous) ->
       ope("PATTCONSTRUCT",
-	  (ast_of_constructor_ref cstr)::List.map ast_of_pattern args)
+	  (ast_of_constructor_ref cstr)::List.map ast_of_cases_pattern args)
 	
 let ast_dependent na aty =
   match na with
@@ -177,18 +178,18 @@ let implicit_of_ref = function
   | RVar id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *)
   | _ -> []
 
-let rec skip_coercion (f,args as app) =
+let rec skip_coercion dest_ref (f,args as app) =
   if !print_coercions then app
   else
     try
-      match f with
-	| RRef (_,r) ->
+      match dest_ref f with
+	| Some r ->
 	    let n = Classops.coercion_params r in
 	    if n >= List.length args then app
 	    else (* We skip a coercion *)
 	      let _,fargs = list_chop n args in
-	      skip_coercion (List.hd fargs,List.tl fargs)
-	| _ -> app
+	      skip_coercion dest_ref (List.hd fargs,List.tl fargs)
+	| None -> app
     with Not_found -> app
 
 let ast_of_app impl f args =
@@ -216,7 +217,8 @@ let ast_of_app impl f args =
 let rec ast_of_raw = function
   | RRef (_,ref) -> ast_of_ref ref
   | RApp (_,f,args) ->
-      let (f,args) = skip_coercion (f,args) in
+      let (f,args) =
+	skip_coercion (function RRef(_,r) -> Some r | _ -> None) (f,args) in
       let astf = ast_of_raw f in
       let astargs = List.map ast_of_raw args in
       (match f with 
@@ -296,7 +298,7 @@ let rec ast_of_raw = function
   | RCast (_,c,t) -> ope("CAST",[ast_of_raw c;ast_of_raw t])
 	
 and ast_of_eqn (ids,pl,c) =
-  ope("EQN", (ast_of_raw c)::(List.map ast_of_pattern pl))
+  ope("EQN", (ast_of_raw c)::(List.map ast_of_cases_pattern pl))
 
 and ast_of_rawopt = function
   | None -> (str "SYNTH")
@@ -730,7 +732,7 @@ let old_bdize at_top env t =
 (* FIN TO EJECT *)
 (******************************************************************)
        
-let bdize at_top env t =
+let ast_of_constr at_top env t =
   let t' =
     if !print_casts then t
     else Reduction.strong (fun _ _ -> strip_outer_cast)
@@ -740,3 +742,79 @@ let bdize at_top env t =
     ast_of_raw (Detyping.detype avoid env t')
   with Detyping.StillDLAM ->
     old_bdize at_top env t'
+
+let rec ast_of_pattern env = function
+  | PRef ref -> ast_of_ref ref
+  | PRel n ->
+      (try match fst (lookup_rel n env) with
+	 | Name id   -> ast_of_ident id
+	 | Anonymous ->
+	     anomaly "ast_of_pattern: index to an anonymous variable"
+       with Not_found ->
+	 let s = "[REL "^(string_of_int (number_of_rels env - n))^"]"
+	 in nvar s)
+
+  | PApp (f,args) ->
+      let (f,args) = 
+	skip_coercion (function PRef r -> Some r | _ -> None)
+	  (f,Array.to_list args) in
+      let astf = ast_of_pattern env f in
+      let astargs = List.map (ast_of_pattern env) args in
+      (match f with 
+	 | PRef ref -> ast_of_app (implicit_of_ref ref) astf astargs
+	 | _        -> ast_of_app [] astf astargs)
+
+  | PSoApp (n,args) ->
+      ope("SOAPP",(ope ("META",[num n])):: 
+		  (List.map (ast_of_constr false env) args))
+
+  | PBinder (BProd,Anonymous,t,c) ->
+      ope("PROD",[ast_of_pattern env t; slam(None,ast_of_pattern env c)])
+  | PBinder (bk,na,t,c) ->
+      let env' = add_rel (na,()) env in
+      let (n,a) = factorize_binder_pattern
+		    env' 1 bk na (ast_of_pattern env t) c in
+      let tag = match bk with
+	  (* LAMBDA et LAMBDALIST se comportent pareil *)
+	| BLambda -> if n=1 then "LAMBDA" else "LAMBDALIST"
+	  (* PROD et PRODLIST doivent être distingués à cause du cas *)
+	  (* non dépendant, pour isoler l'implication; peut-être un *)
+	  (* constructeur ARROW serait-il plus justifié ? *) 
+	| BProd -> if n=1 then "PROD" else "PRODLIST" 
+      in
+      ope(tag,[ast_of_pattern env t;a])
+
+  | PLet (id,a,t,c) ->
+      let c' = ast_of_pattern (add_rel (Name id,()) env) c in
+      ope("LET",[ast_of_pattern env a; 	slam(Some (string_of_id id),c')])
+		
+
+  | PCase (typopt,tm,bv) ->
+      warning "Old Case syntax";
+      ope("MUTCASE",(ast_of_patopt env typopt)
+	    ::(ast_of_pattern env tm)
+	    ::(Array.to_list (Array.map (ast_of_pattern env) bv)))
+
+  | PSort s ->
+      (match s with
+	 | RProp Null -> ope("PROP",[])
+	 | RProp Pos -> ope("SET",[])
+	 | RType -> ope("TYPE",[]))
+
+  | PMeta (Some n) -> ope("META",[num n])
+  | PMeta None -> ope("ISEVAR",[])
+	
+and ast_of_patopt env = function
+  | None -> (str "SYNTH")
+  | Some p -> ast_of_pattern env p
+
+and factorize_binder_pattern env n oper na aty c =
+  let (p,body) = match c with
+    | PBinder(oper',na',ty',c')
+	when (oper = oper') & (aty = ast_of_pattern env ty')
+	  & not (na' = Anonymous & oper = BProd)
+	  ->
+	factorize_binder_pattern (add_rel (na',()) env) (n+1) oper na' aty c'
+    | _ -> (n,ast_of_pattern env c)
+  in
+  (p,slam(stringopt_of_name na, body))
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index 51ab2d5176..4980afd587 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -45,7 +45,7 @@ Syntax constr
 
 (* Things parsed in command1 *)
   level 1:
-    soap [(XTRA "$SOAPP" $lc1 ($LIST $cl))]
+    soap [(SOAPP $lc1 ($LIST $cl))]
       -> [ [<hov 0> "(" $lc1 ")@[" (NECOMMANDLIST ($LIST $cl)) "]"] ]
   | let_K [(ABST #Core#let.cci $M [<>]$N)]
       -> [ [<hov 0> "[_=" $M "]" [0 1] $N:E ] ]
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 7d9d3530af..f0b4e81add 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -11,6 +11,7 @@ open Inductive
 open Evd
 open Reduction
 open Typing
+open Pattern
 open Tacmach
 open Proof_trees
 open Pfedit
@@ -702,7 +703,7 @@ let possible_resolve db_list local_db cl =
 let decomp_unary_term c gls = 
   let typc = pf_type_of gls c in 
   let hd = List.hd (head_constr typc) in 
-  if Pattern.is_conjunction hd then 
+  if Hipattern.is_conjunction hd then 
     simplest_case c gls 
   else 
     errorlabstrm "Auto.decomp_unary_term" [<'sTR "not a unary type" >] 
@@ -710,7 +711,7 @@ let decomp_unary_term c gls =
 let decomp_empty_term c gls = 
   let typc = pf_type_of gls c in 
   let (hd,_) = decomp_app typc in 
-  if Pattern.is_empty_type hd then 
+  if Hipattern.is_empty_type hd then 
     simplest_case c gls 
   else 
     errorlabstrm "Auto.decomp_empty_term" [<'sTR "not an empty type" >] 
@@ -858,7 +859,7 @@ let compileAutoArg contac = function
 	 tclFIRST 
            (List.map2 
               (fun id typ -> 
-                 if (Pattern.is_conjunction (hd_of_prod typ)) then 
+                 if (Hipattern.is_conjunction (hd_of_prod typ)) then 
 		   (tclTHEN
                       (tclTHEN (simplest_elim (mkVar id)) 
                          (clear_one id))
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 3dbbacea69..e238f5f79d 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -3,7 +3,7 @@
 
 open Term
 open Termdn
-open Rawterm
+open Pattern
 
 (* Discrimination nets with bounded depth.
    See the module dn.ml for further explanations.
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 0ca3f6b2a8..a21b3e6d7c 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -128,8 +128,8 @@ open Pcoq
 
 (* two patterns - one for the type, and one for the type of the type *)
 type destructor_pattern = {
-  d_typ: Rawterm.constr_pattern; 
-  d_sort: Rawterm.constr_pattern }
+  d_typ: constr_pattern; 
+  d_sort: constr_pattern }
     
 type ('a,'b) location = Hyp of 'a | Concl of 'b
 
@@ -222,11 +222,11 @@ let _ =
 	     add_destructor_hint na
                (match loc with
 		  | Hyp b ->
-		      Hyp(b,{d_typ=pat;d_sort=PMeta(new_meta())},
-			  { d_typ=PMeta(new_meta());
-		       	    d_sort=PMeta(new_meta()) })
+		      Hyp(b,{d_typ=pat;d_sort=PMeta(Some (new_meta()))},
+			  { d_typ=PMeta(Some (new_meta()));
+		       	    d_sort=PMeta(Some (new_meta())) })
 		  | Concl () ->
-		      Concl({d_typ=pat;d_sort=PMeta(new_meta())}))
+		      Concl({d_typ=pat;d_sort=PMeta(Some (new_meta()))}))
                pri code
        | _ -> bad_vernac_args "HintDestruct")
 
@@ -234,13 +234,13 @@ let match_dpat dp cls gls =
   let cltyp = clause_type cls gls in
   match (cls,dp) with
     | (Some id,Hyp(_,hypd,concld)) ->
-        (somatch None hypd.d_typ cltyp)@
-        (somatch None hypd.d_sort (pf_type_of gls cltyp))@
-        (somatch None concld.d_typ (pf_concl gls))@
-        (somatch None concld.d_sort (pf_type_of gls (pf_concl gls)))
+        (matches hypd.d_typ cltyp)@
+        (matches hypd.d_sort (pf_type_of gls cltyp))@
+        (matches concld.d_typ (pf_concl gls))@
+        (matches concld.d_sort (pf_type_of gls (pf_concl gls)))
     | (None,Concl concld) ->
-        (somatch None concld.d_typ (pf_concl gls))@
-        (somatch None concld.d_sort (pf_type_of gls (pf_concl gls)))
+        (matches concld.d_typ (pf_concl gls))@
+        (matches concld.d_sort (pf_type_of gls (pf_concl gls)))
     | _ -> error "ApplyDestructor"
 
 let applyDestructor cls discard dd gls =
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 69c4104d9f..4abff0e4d2 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -9,7 +9,7 @@ open Term
 open Reduction
 open Proof_trees
 open Clenv
-open Pattern
+open Hipattern
 open Tacmach
 open Tacticals
 open Tactics
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ff62150a0b..e1fe98148c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -18,6 +18,7 @@ open Proof_trees
 open Logic
 open Wcclausenv
 open Pattern
+open Hipattern
 open Tacticals
 open Tactics
 open Tacinterp
@@ -526,12 +527,12 @@ let rec build_discriminator sigma env dirn c sort = function
   | _ -> assert false
 
 let dest_somatch_eq eqn eq_pat =
-  match dest_somatch eqn eq_pat with
+  match matches eqn eq_pat with
     | [t;x;y] -> (t,x,y)
     | _ -> anomaly "dest_somatch_eq: an eq pattern should match 3 terms"
 	  
 let find_eq_data_decompose eqn =
-  if (somatches eqn eq_pattern) then
+  if (matches eqn eq_pattern) then
     (eq, dest_somatch_eq eqn eq_pattern)
   else if (somatches eqn eqT_pattern) then
     (eqT, dest_somatch_eq eqn eqT_pattern)
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index e762531d42..09b7729504 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -7,6 +7,7 @@ open Generic
 open Term
 open Libobject
 open Library
+open Pattern
 
 (* Named, bounded-depth, term-discrimination nets.
    Implementation:
@@ -20,12 +21,12 @@ open Library
    Eduardo (5/8/97) *)
 
 type ('na,'a) t = {
-  mutable table : ('na,Rawterm.constr_pattern * 'a) Gmap.t;
-  mutable patterns : (Rawterm.constr_label option,'a Btermdn.t) Gmap.t }
+  mutable table : ('na,constr_pattern * 'a) Gmap.t;
+  mutable patterns : (constr_label option,'a Btermdn.t) Gmap.t }
 
 type ('na,'a) frozen_t = 
-    ('na,Rawterm.constr_pattern * 'a) Gmap.t
-    * (Rawterm.constr_label option,'a Btermdn.t) Gmap.t
+    ('na,constr_pattern * 'a) Gmap.t
+    * (constr_label option,'a Btermdn.t) Gmap.t
 
 let create () =
   { table = Gmap.empty;
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6425bdc28f..6169847c16 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -118,16 +118,13 @@ let clause_type cls gl =
 
 (* Functions concerning matching of clausal environments *)
 
-let matches gls n pat =
+let gl_is_matching gls pat n =
   let (wc,_) = startWalk gls in 
-  somatches_conv (w_env wc) (w_Underlying wc) n pat
+  is_matching_conv (w_env wc) (w_Underlying wc) pat n
 
-let dest_match gls n m =
-  let mvs     = collect_metas m in
+let gl_matches gls pat n =
   let (wc,_)  = startWalk gls in
-  let (mvb,_) = Clenv.unify_0 [] wc m n in 
-  List.map (fun x -> List.assoc x mvb) mvs
-
+  matches_conv (w_env wc) (w_Underlying wc) pat n
 
 (* [OnCL clausefinder clausetac]
  * executes the clausefinder to find the clauses, and then executes the
@@ -191,10 +188,11 @@ si après Intros la conclusion matche le pattern.
 *)
 
 let conclPattern concl pat tacast gl = 
-  let constr_bindings = Pattern.somatch None pat concl in
+  let constr_bindings = Pattern.matches pat concl in
   let ast_bindings = 
     List.map 
-      (fun (i,c) -> (i, Termast.bdize false (assumptions_for_print []) c))
+      (fun (i,c) ->
+	 (i, Termast.ast_of_constr false (assumptions_for_print []) c))
       constr_bindings in 
   let tacast' = Coqast.subst_meta ast_bindings tacast in
   Tacinterp.interp tacast' gl
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0bc6860b28..66dd8b1ad6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -19,7 +19,7 @@ open Proof_trees
 open Logic
 open Clenv
 open Tacticals
-open Pattern
+open Hipattern
 
 exception Bound
 
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 957543e16d..ec621c4a74 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -5,7 +5,7 @@ open Util
 open Generic
 open Names
 open Term
-open Rawterm
+open Pattern
 
 (* Discrimination nets of terms.
    See the module dn.ml for further explanations.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4c1b0e4b71..8b1fc69f3f 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -26,17 +26,17 @@ let explain_unbound_rel k ctx n =
      'sTR"The reference "; 'iNT n; 'sTR" is free" >]
 
 let explain_cant_execute k ctx c =
-  let tc = gentermpr k ctx c in
+  let tc = prterm_env ctx c in
   [< 'sTR"Cannot execute term:"; 'bRK(1,1); tc >]
 
 let explain_not_type k ctx c =
   let pe = pr_ne_env [< 'sTR"In environment" >] k ctx in
-  let pc = gentermpr k ctx c in
+  let pc = prterm_env ctx c in
   [< pe; 'cUT; 'sTR "the term"; 'bRK(1,1); pc; 'sPC;
      'sTR"should be typed by Set, Prop or Type." >];;
 
 let explain_bad_assumption k ctx c =
-  let pc = gentermpr k ctx c in
+  let pc = prterm_env ctx c in
   [< 'sTR "Cannot declare a variable or hypothesis over the term";
      'bRK(1,1); pc; 'sPC; 'sTR "because this term is not a type." >];;
 
@@ -46,8 +46,8 @@ let explain_reference_variables id =
 
 let msg_bad_elimination ctx k = function
   | Some(ki,kp,explanation) ->
-      let pki = gentermpr k ctx ki in
-      let pkp = gentermpr k ctx kp in
+      let pki = prterm_env ctx ki in
+      let pkp = prterm_env ctx kp in
       (hOV 0 
          [< 'fNL; 'sTR "Elimination of an inductive object of sort : ";
             pki; 'bRK(1,0);
@@ -57,11 +57,11 @@ let msg_bad_elimination ctx k = function
       [<>]
 
 let explain_elim_arity k ctx ind aritylst c p pt okinds = 
-  let pi = gentermpr k ctx ind in
-  let ppar = prlist_with_sep pr_coma (gentermpr k ctx) aritylst in
-  let pc = gentermpr k ctx c in
-  let pp = gentermpr k ctx p in
-  let ppt = gentermpr k ctx pt in
+  let pi = prterm_env ctx ind in
+  let ppar = prlist_with_sep pr_coma (prterm_env ctx) aritylst in
+  let pc = prterm_env ctx c in
+  let pp = prterm_env ctx p in
+  let ppt = prterm_env ctx pt in
   [< 'sTR "Incorrect elimination of"; 'bRK(1,1); pc; 'sPC;
      'sTR "in the inductive type"; 'bRK(1,1); pi; 'fNL;
      'sTR "The elimination predicate"; 'bRK(1,1); pp; 'sPC;
@@ -70,23 +70,23 @@ let explain_elim_arity k ctx ind aritylst c p pt okinds =
      msg_bad_elimination ctx k okinds >]
 
 let explain_case_not_inductive k ctx c ct =
-  let pc = gentermpr k ctx c in
-  let pct = gentermpr k ctx ct in
+  let pc = prterm_env ctx c in
+  let pct = prterm_env ctx ct in
   [< 'sTR "In Cases expression"; 'bRK(1,1); pc; 'sPC; 
      'sTR "has type"; 'bRK(1,1); pct; 'sPC; 
      'sTR "which is not an inductive definition" >]
   
 let explain_number_branches k ctx c ct expn =
-  let pc = gentermpr k ctx c in
-  let pct = gentermpr k ctx ct in
+  let pc = prterm_env ctx c in
+  let pct = prterm_env ctx ct in
   [< 'sTR "Cases on term"; 'bRK(1,1); pc; 'sPC ;
      'sTR "of type"; 'bRK(1,1); pct; 'sPC;
      'sTR "expects ";  'iNT expn; 'sTR " branches" >]
 
 let explain_ill_formed_branch k ctx c i actty expty =
-  let pc = gentermpr k ctx c in
-  let pa = gentermpr k ctx actty in
-  let pe = gentermpr k ctx expty in
+  let pc = prterm_env ctx c in
+  let pa = prterm_env ctx actty in
+  let pe = prterm_env ctx expty in
   [< 'sTR "In Cases expression on term"; 'bRK(1,1); pc;
      'sPC; 'sTR "the branch " ; 'iNT (i+1);
      'sTR " has type"; 'bRK(1,1); pa ; 'sPC; 
@@ -94,8 +94,8 @@ let explain_ill_formed_branch k ctx c i actty expty =
 
 let explain_generalization k ctx (name,var) c =
   let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
-  let pv = gentermpr k ctx (body_of_type var) in
-  let pc = gentermpr k (add_rel (name,var) ctx) c in
+  let pv = prterm_env ctx (body_of_type var) in
+  let pc = prterm_env (add_rel (name,var) ctx) c in
   [< 'sTR"Illegal generalization: "; pe; 'fNL;
      'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC;
      'sTR"over"; 'bRK(1,1); pc; 'sPC;
@@ -103,9 +103,9 @@ let explain_generalization k ctx (name,var) c =
 
 let explain_actual_type k ctx c ct pt =
   let pe = pr_ne_env [< 'sTR"In environment" >] k ctx in
-  let pc = gentermpr k ctx c in
-  let pct = gentermpr k ctx ct in
-  let pt = gentermpr k ctx pt in
+  let pc = prterm_env ctx c in
+  let pct = prterm_env ctx ct in
+  let pt = prterm_env ctx pt in
   [< pe; 'fNL;
      'sTR"The term"; 'bRK(1,1); pc ; 'sPC ;
      'sTR"does not have type"; 'bRK(1,1); pt; 'fNL;
@@ -113,14 +113,14 @@ let explain_actual_type k ctx c ct pt =
 
 let explain_cant_apply k ctx s rator randl =
   let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
-  let pr = gentermpr k ctx rator.uj_val in
-  let prt = gentermpr k ctx rator.uj_type in
+  let pr = prterm_env ctx rator.uj_val in
+  let prt = prterm_env ctx rator.uj_type in
   let term_string = if List.length randl > 1 then "terms" else "term" in
   let appl = 
     prlist_with_sep pr_fnl
       (fun c ->
-         let pc = gentermpr k ctx c.uj_val in
-         let pct = gentermpr k ctx c.uj_type in
+         let pc = prterm_env ctx c.uj_val in
+         let pct = prterm_env ctx c.uj_type in
          hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl 
   in
   [< 'sTR"Illegal application ("; 'sTR s; 'sTR"): "; pe; 'fNL;
@@ -131,7 +131,7 @@ let explain_cant_apply k ctx s rator randl =
 
 (* (co)fixpoints *)
 let explain_ill_formed_rec_body k ctx str lna i vdefs =
-  let pvd = gentermpr k ctx vdefs.(i) in
+  let pvd = prterm_env ctx vdefs.(i) in
   let s =
     match List.nth lna i with Name id -> string_of_id id | Anonymous -> "_" in
   [< str; 'fNL; 'sTR"The ";
@@ -141,30 +141,30 @@ let explain_ill_formed_rec_body k ctx str lna i vdefs =
      'sTR "is not well-formed" >]
     
 let explain_ill_typed_rec_body k ctx i lna vdefj vargs =
-  let pvd = gentermpr k ctx (vdefj.(i)).uj_val in
-  let pvdt = gentermpr k ctx (vdefj.(i)).uj_type in
-  let pv = gentermpr k ctx (body_of_type vargs.(i)) in
+  let pvd = prterm_env ctx (vdefj.(i)).uj_val in
+  let pvdt = prterm_env ctx (vdefj.(i)).uj_type in
+  let pv = prterm_env ctx (body_of_type vargs.(i)) in
   [< 'sTR"The " ;
      if Array.length vdefj = 1 then [<>] else [<'iNT (i+1); 'sTR "-th">];
      'sTR"recursive definition" ; 'sPC; pvd; 'sPC;
      'sTR "has type"; 'sPC; pvdt;'sPC; 'sTR "it should be"; 'sPC; pv >]
 
 let explain_not_inductive k ctx c =
-  let pc = gentermpr k ctx c in
+  let pc = prterm_env ctx c in
   [< 'sTR"The term"; 'bRK(1,1); pc; 'sPC;
      'sTR "is not an inductive definition" >]
 
 let explain_ml_case k ctx mes c ct br brt =
-  let pc = gentermpr k ctx c in
-  let pct = gentermpr k ctx ct in
+  let pc = prterm_env ctx c in
+  let pct = prterm_env ctx ct in
   let expln =
     match mes with
       | "Inductive" -> [< pct; 'sTR "is not an inductive definition">]
       | "Predicate" -> [< 'sTR "ML case not allowed on a predicate">]
       | "Absurd" -> [< 'sTR "Ill-formed case expression on an empty type" >]
       | "Decomp" ->
-          let plf = gentermpr k ctx br in
-          let pft = gentermpr k ctx brt in
+          let plf = prterm_env ctx br in
+          let pft = prterm_env ctx brt in
           [< 'sTR "The branch "; plf; 'wS 1; 'cUT; 'sTR "has type "; pft;
              'wS 1; 'cUT;
              'sTR "does not correspond to the inductive definition" >]
@@ -177,12 +177,12 @@ let explain_ml_case k ctx mes c ct br brt =
            'sTR "which is an inductive predicate."; 'fNL; expln >]
 
 let explain_cant_find_case_type k ctx c =
-  let pe = gentermpr k ctx c in
+  let pe = prterm_env ctx c in
   hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 'wS 1; pe >]
 
 (***
 let explain_cant_find_case_type_loc loc k ctx c =
-  let pe = gentermpr k ctx c in
+  let pe = prterm_env ctx c in
   user_err_loc
     (loc,"pretype",
      hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 
@@ -191,14 +191,14 @@ let explain_cant_find_case_type_loc loc k ctx c =
 
 let explain_occur_check k ctx ev rhs =
   let id = "?" ^ string_of_int ev in
-  let pt = gentermpr k ctx rhs in
+  let pt = prterm_env ctx rhs in
   [< 'sTR"Occur check failed: tried to define "; 'sTR id;
      'sTR" with term"; 'bRK(1,1); pt >]
 
 let explain_not_clean k ctx ev t =
   let c = Rel (Intset.choose (free_rels t)) in
   let id = "?" ^ string_of_int ev in
-  let var = gentermpr k ctx c in
+  let var = prterm_env ctx c in
   [< 'sTR"Tried to define "; 'sTR id;
      'sTR" with a term using variable "; var; 'sPC;
      'sTR"which is not in its scope." >]
@@ -223,15 +223,15 @@ let explain_wrong_numarg_of_constructor k ctx cstr n =
     'sTR " expects " ; 'iNT n ; 'sTR " arguments. ">]
 
 let explain_wrong_predicate_arity k ctx pred nondep_arity dep_arity=
-  let pp = gentermpr k ctx pred in
+  let pp = prterm_env ctx pred in
   [<'sTR "The elimination predicate " ; pp; 'cUT;
     'sTR "should be of arity " ;
     'iNT nondep_arity ; 'sTR " (for non dependent case)  or " ;
     'iNT dep_arity ; 'sTR " (for dependent case).">]
 
 let explain_needs_inversion k ctx x t =
-  let px = gentermpr k ctx x in
-  let pt = gentermpr k ctx t in
+  let px = prterm_env ctx x in
+  let pt = prterm_env ctx t in
   [< 'sTR "Sorry, I need inversion to compile pattern matching of term ";
      px ; 'sTR " of type: "; pt>]
 
@@ -331,22 +331,22 @@ let explain_refiner_error = function
 
 let error_non_strictly_positive k lna c v  =
   let env = assumptions_for_print lna in
-  let pc = gentermpr k env c in
-  let pv = gentermpr k env v in
+  let pc = prterm_env env c in
+  let pv = prterm_env env v in
   [< 'sTR "Non strictly positive occurrence of "; pv; 'sTR " in";
      'bRK(1,1); pc >]
 
 let error_ill_formed_inductive k lna c v =
   let env = assumptions_for_print lna in
-  let pc = gentermpr k env c in
-  let pv = gentermpr k env v in
+  let pc = prterm_env env c in
+  let pv = prterm_env env v in
   [< 'sTR "Not enough arguments applied to the "; pv;
      'sTR " in"; 'bRK(1,1); pc >]
 
 let error_ill_formed_constructor k lna c v =
   let env = assumptions_for_print lna in
-  let pc = gentermpr k env c in
-  let pv = gentermpr k env v in
+  let pc = prterm_env env c in
+  let pv = prterm_env env v in
   [< 'sTR "The conclusion of"; 'bRK(1,1); pc; 'bRK(1,1); 
      'sTR "is not valid;"; 'bRK(1,1); 'sTR "it must be built from "; pv >]
 
@@ -360,9 +360,9 @@ let str_of_nth n =
 
 let error_bad_ind_parameters k lna c n v1 v2  =
   let env = assumptions_for_print lna in
-  let pc = gentermpr_at_top k env c in
-  let pv1 = gentermpr k env v1 in
-  let pv2 = gentermpr k env v2 in
+  let pc = prterm_env_at_top env c in
+  let pv1 = prterm_env env v1 in
+  let pv2 = prterm_env env v2 in
   [< 'sTR ("The "^(str_of_nth n)^" argument of "); pv2; 'bRK(1,1);
      'sTR "must be "; pv1; 'sTR " in"; 'bRK(1,1); pc >]