debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkes

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

20 files changed, 239 insertions, 118 deletions

diff --git a/.depend b/.depend
index 9673886b8..70c7cba1a 100644
--- a/.depend
+++ b/.depend
@@ -28,7 +28,7 @@ kernel/term.cmi: kernel/generic.cmi kernel/names.cmi lib/pp.cmi \
 kernel/type_errors.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi 
 kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
-    kernel/term.cmi kernel/univ.cmi 
+    kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
 lib/system.cmi: lib/pp.cmi 
@@ -125,6 +125,7 @@ tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi parsing/coqast.cmi \
     kernel/names.cmi proofs/proof_trees.cmi kernel/sign.cmi \
     proofs/tacmach.cmi kernel/term.cmi lib/util.cmi 
 tactics/btermdn.cmi: kernel/generic.cmi kernel/term.cmi 
+tactics/dhyp.cmi: kernel/names.cmi proofs/tacmach.cmi 
 tactics/dn.cmi: lib/tlm.cmi 
 tactics/elim.cmi: kernel/names.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \
     tactics/tacticals.cmi kernel/term.cmi 
@@ -137,9 +138,9 @@ tactics/pattern.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/term.cmi lib/util.cmi 
 tactics/stock.cmi: kernel/names.cmi 
 tactics/tacentries.cmi: proofs/proof_trees.cmi proofs/tacmach.cmi 
-tactics/tacticals.cmi: proofs/clenv.cmi kernel/names.cmi tactics/pattern.cmi \
-    proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi kernel/term.cmi tactics/wcclausenv.cmi 
+tactics/tacticals.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/names.cmi \
+    tactics/pattern.cmi proofs/proof_trees.cmi kernel/reduction.cmi \
+    kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi tactics/wcclausenv.cmi 
 tactics/tactics.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/environ.cmi \
     kernel/evd.cmi kernel/names.cmi proofs/proof_trees.cmi \
     kernel/reduction.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
@@ -233,11 +234,13 @@ kernel/generic.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi \
 kernel/generic.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx \
     kernel/generic.cmi 
 kernel/indtypes.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
-    kernel/inductive.cmi kernel/instantiate.cmi kernel/reduction.cmi \
-    kernel/sign.cmi kernel/term.cmi lib/util.cmi kernel/indtypes.cmi 
+    kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi \
+    kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi kernel/typeops.cmi \
+    lib/util.cmi kernel/indtypes.cmi 
 kernel/indtypes.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
-    kernel/inductive.cmx kernel/instantiate.cmx kernel/reduction.cmx \
-    kernel/sign.cmx kernel/term.cmx lib/util.cmx kernel/indtypes.cmi 
+    kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx \
+    kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx kernel/typeops.cmx \
+    lib/util.cmx kernel/indtypes.cmi 
 kernel/inductive.cmo: kernel/generic.cmi kernel/names.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/univ.cmi lib/util.cmi kernel/inductive.cmi 
 kernel/inductive.cmx: kernel/generic.cmx kernel/names.cmx kernel/sign.cmx \
@@ -333,13 +336,15 @@ library/declare.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
     library/indrec.cmi kernel/inductive.cmi library/lib.cmi \
     library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
     kernel/reduction.cmi kernel/sign.cmi library/summary.cmi kernel/term.cmi \
-    kernel/univ.cmi lib/util.cmi library/declare.cmi 
+    kernel/type_errors.cmi kernel/typeops.cmi kernel/univ.cmi lib/util.cmi \
+    library/declare.cmi 
 library/declare.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \
     kernel/generic.cmx library/global.cmx library/impargs.cmx \
     library/indrec.cmx kernel/inductive.cmx library/lib.cmx \
     library/libobject.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
     kernel/reduction.cmx kernel/sign.cmx library/summary.cmx kernel/term.cmx \
-    kernel/univ.cmx lib/util.cmx library/declare.cmi 
+    kernel/type_errors.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \
+    library/declare.cmi 
 library/discharge.cmo: library/declare.cmi library/lib.cmi \
     library/discharge.cmi 
 library/discharge.cmx: library/declare.cmx library/lib.cmx \
@@ -674,20 +679,22 @@ proofs/tacmach.cmx: parsing/ast.cmx parsing/astterm.cmx library/declare.cmx \
     proofs/tacmach.cmi 
 scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo 
 scripts/coqmktop.cmx: config/coq_config.cmx scripts/tolink.cmx 
-tactics/auto.cmo: tactics/btermdn.cmi proofs/clenv.cmi library/declare.cmi \
-    tactics/dhyp.cmi kernel/evd.cmi kernel/generic.cmi library/global.cmi \
-    tactics/hiddentac.cmi kernel/inductive.cmi library/lib.cmi \
-    library/libobject.cmi library/library.cmi kernel/names.cmi \
-    tactics/pattern.cmi proofs/pfedit.cmi lib/pp.cmi proofs/proof_trees.cmi \
+tactics/auto.cmo: parsing/astterm.cmi tactics/btermdn.cmi proofs/clenv.cmi \
+    parsing/coqast.cmi library/declare.cmi tactics/dhyp.cmi kernel/evd.cmi \
+    kernel/generic.cmi library/global.cmi tactics/hiddentac.cmi \
+    kernel/inductive.cmi library/lib.cmi library/libobject.cmi \
+    library/library.cmi kernel/names.cmi tactics/pattern.cmi \
+    proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
     kernel/reduction.cmi kernel/sign.cmi library/summary.cmi \
     proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \
     tactics/tactics.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
     toplevel/vernacinterp.cmi tactics/auto.cmi 
-tactics/auto.cmx: tactics/btermdn.cmx proofs/clenv.cmx library/declare.cmx \
-    tactics/dhyp.cmx kernel/evd.cmx kernel/generic.cmx library/global.cmx \
-    tactics/hiddentac.cmx kernel/inductive.cmx library/lib.cmx \
-    library/libobject.cmx library/library.cmx kernel/names.cmx \
-    tactics/pattern.cmx proofs/pfedit.cmx lib/pp.cmx proofs/proof_trees.cmx \
+tactics/auto.cmx: parsing/astterm.cmx tactics/btermdn.cmx proofs/clenv.cmx \
+    parsing/coqast.cmx library/declare.cmx tactics/dhyp.cmx kernel/evd.cmx \
+    kernel/generic.cmx library/global.cmx tactics/hiddentac.cmx \
+    kernel/inductive.cmx library/lib.cmx library/libobject.cmx \
+    library/library.cmx kernel/names.cmx tactics/pattern.cmx \
+    proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
     kernel/reduction.cmx kernel/sign.cmx library/summary.cmx \
     proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \
     tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
@@ -696,16 +703,18 @@ tactics/btermdn.cmo: tactics/dn.cmi kernel/term.cmi tactics/termdn.cmi \
     tactics/btermdn.cmi 
 tactics/btermdn.cmx: tactics/dn.cmx kernel/term.cmx tactics/termdn.cmx \
     tactics/btermdn.cmi 
-tactics/dhyp.cmo: parsing/ast.cmi proofs/clenv.cmi kernel/generic.cmi \
-    library/lib.cmi library/libobject.cmi library/library.cmi \
-    kernel/names.cmi tactics/nbtermdn.cmi tactics/pattern.cmi lib/pp.cmi \
+tactics/dhyp.cmo: parsing/ast.cmi proofs/clenv.cmi parsing/coqast.cmi \
+    kernel/environ.cmi kernel/generic.cmi library/global.cmi library/lib.cmi \
+    library/libobject.cmi library/library.cmi kernel/names.cmi \
+    tactics/nbtermdn.cmi tactics/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \
     proofs/proof_trees.cmi kernel/reduction.cmi library/summary.cmi \
     proofs/tacinterp.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
     tactics/tactics.cmi kernel/term.cmi lib/util.cmi \
     toplevel/vernacinterp.cmi tactics/dhyp.cmi 
-tactics/dhyp.cmx: parsing/ast.cmx proofs/clenv.cmx kernel/generic.cmx \
-    library/lib.cmx library/libobject.cmx library/library.cmx \
-    kernel/names.cmx tactics/nbtermdn.cmx tactics/pattern.cmx lib/pp.cmx \
+tactics/dhyp.cmx: parsing/ast.cmx proofs/clenv.cmx parsing/coqast.cmx \
+    kernel/environ.cmx kernel/generic.cmx library/global.cmx library/lib.cmx \
+    library/libobject.cmx library/library.cmx kernel/names.cmx \
+    tactics/nbtermdn.cmx tactics/pattern.cmx parsing/pcoq.cmx lib/pp.cmx \
     proofs/proof_trees.cmx kernel/reduction.cmx library/summary.cmx \
     proofs/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
     tactics/tactics.cmx kernel/term.cmx lib/util.cmx \
@@ -748,18 +757,22 @@ tactics/tacentries.cmo: proofs/proof_trees.cmi proofs/tacmach.cmi \
     tactics/tacticals.cmi tactics/tactics.cmi tactics/tacentries.cmi 
 tactics/tacentries.cmx: proofs/proof_trees.cmx proofs/tacmach.cmx \
     tactics/tacticals.cmx tactics/tactics.cmx tactics/tacentries.cmi 
-tactics/tacticals.cmo: proofs/clenv.cmi library/declare.cmi \
-    kernel/environ.cmi kernel/generic.cmi library/global.cmi \
-    library/indrec.cmi kernel/inductive.cmi kernel/names.cmi \
-    tactics/pattern.cmi lib/pp.cmi parsing/pretty.cmi proofs/proof_trees.cmi \
-    kernel/reduction.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \
-    lib/util.cmi tactics/wcclausenv.cmi tactics/tacticals.cmi 
-tactics/tacticals.cmx: proofs/clenv.cmx library/declare.cmx \
-    kernel/environ.cmx kernel/generic.cmx library/global.cmx \
-    library/indrec.cmx kernel/inductive.cmx kernel/names.cmx \
-    tactics/pattern.cmx lib/pp.cmx parsing/pretty.cmx proofs/proof_trees.cmx \
-    kernel/reduction.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \
-    lib/util.cmx tactics/wcclausenv.cmx tactics/tacticals.cmi 
+tactics/tacticals.cmo: proofs/clenv.cmi parsing/coqast.cmi \
+    library/declare.cmi kernel/environ.cmi kernel/generic.cmi \
+    library/global.cmi library/indrec.cmi kernel/inductive.cmi \
+    kernel/names.cmi tactics/pattern.cmi lib/pp.cmi parsing/pretty.cmi \
+    proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \
+    proofs/tacinterp.cmi proofs/tacmach.cmi kernel/term.cmi \
+    parsing/termast.cmi lib/util.cmi tactics/wcclausenv.cmi \
+    tactics/tacticals.cmi 
+tactics/tacticals.cmx: proofs/clenv.cmx parsing/coqast.cmx \
+    library/declare.cmx kernel/environ.cmx kernel/generic.cmx \
+    library/global.cmx library/indrec.cmx kernel/inductive.cmx \
+    kernel/names.cmx tactics/pattern.cmx lib/pp.cmx parsing/pretty.cmx \
+    proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
+    proofs/tacinterp.cmx proofs/tacmach.cmx kernel/term.cmx \
+    parsing/termast.cmx lib/util.cmx tactics/wcclausenv.cmx \
+    tactics/tacticals.cmi 
 tactics/tactics.cmo: parsing/ast.cmi parsing/astterm.cmi proofs/clenv.cmi \
     library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     library/global.cmi library/indrec.cmi kernel/inductive.cmi \
diff --git a/Makefile b/Makefile
index 68f8d4a09..0caff0f35 100644
--- a/Makefile
+++ b/Makefile
@@ -96,6 +96,7 @@ TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
         tactics/nbtermdn.cmo tactics/stock.cmo tactics/pattern.cmo \
 	tactics/wcclausenv.cmo tactics/tacticals.cmo tactics/tactics.cmo \
         tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo
+#	tactics/dhyp.cmo tactics/auto.cmo
 
 TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \
          toplevel/metasyntax.cmo toplevel/command.cmo toplevel/class.cmo \
diff --git a/kernel/generic.ml b/kernel/generic.ml
index 6b38b72ff..0484a801d 100644
--- a/kernel/generic.ml
+++ b/kernel/generic.ml
@@ -337,7 +337,17 @@ let global_varsl l constr =
 let global_vars constr = global_varsl [] constr
 
 let global_vars_set constr = 
-  List.fold_left (fun s x -> Idset.add x s) Idset.empty (global_vars constr)
+  let rec filtrec acc = function
+    | VAR id             -> Idset.add id acc
+    | DOP1(oper,c)       -> filtrec acc c
+    | DOP2(oper,c1,c2)   -> filtrec (filtrec acc c1) c2
+    | DOPN(oper,cl)      -> Array.fold_left filtrec acc cl
+    | DOPL(oper,cl)      -> List.fold_left filtrec acc cl
+    | DLAM(_,c)          -> filtrec acc c
+    | DLAMV(_,v)         -> Array.fold_left filtrec acc v
+    | _                  -> acc
+  in 
+  filtrec Idset.empty constr
 
 (* alpha equality for generic terms : checks first if M and M' are equal,
    otherwise checks equality forgetting the name annotation of DLAM and DLAMV*)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a34c98832..da9604699 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -2,6 +2,7 @@
 (* $Id$ *)
 
 open Util
+open Names
 open Generic
 open Term
 open Inductive
@@ -9,6 +10,7 @@ open Sign
 open Environ
 open Instantiate
 open Reduction
+open Typeops
 
 (* In the following, each time an [evar_map] is required, then [Evd.empty]
    is given, since inductive types are typed in an environment without 
@@ -49,7 +51,7 @@ type ill_formed_ind =
 exception IllFormedInd of ill_formed_ind
 
 let explain_ind_err ntyp lna nbpar c err = 
-  let (lpar,c') = decompose_prod_n nbpar c in
+  let (lpar,c') = mind_extract_params nbpar c in
   let env = (List.map fst lpar)@lna in
   match err with
     | NonPos kt -> 
@@ -94,7 +96,7 @@ let abstract_mind_lc env ntyps npars lc =
     in 
     Array.map (compose (nf_beta env Evd.empty) (substl make_abs)) lC
 
-let decomp_par n c = snd (decompose_prod_n n c)
+let decomp_par n c = snd (mind_extract_params n c)
       
 let listrec_mconstr env ntypes nparams i indlc =
   (* check the inductive types occur positively in C *)
@@ -267,10 +269,17 @@ let cci_inductive env env_ar kind nparams finite inds cst =
       mind_listrec = recargs;
       mind_finite = finite }
   in
+  let ids = 
+    List.fold_left 
+      (fun acc (_,ar,_,_,_,lc) -> 
+	 Idset.union (global_vars_set ar.body) 
+	   (Idset.union (global_vars_set lc) acc))
+      Idset.empty inds
+  in
   let packets = Array.of_list (list_map_i one_packet 1 inds) in
   { mind_kind = kind;
     mind_ntypes = ntypes;
-    mind_hyps = var_context env;
+    mind_hyps = keep_hyps (var_context env) ids;
     mind_packets = packets;
     mind_constraints = cst;
     mind_singl = None;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 433a2c1d9..5ab2886a9 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -121,7 +121,8 @@ let mind_check_names mie =
    declaration, and checks that they are all present (and all the same)
    for all the given types. *)
 
-let mind_extract_params = decompose_prod_n
+let mind_extract_params n c = 
+  let (l,c') = decompose_prod_n n c in (List.rev l,c')
   
 let extract nparams c =
   try mind_extract_params nparams c 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8f1ad3787..efa860fa2 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -280,11 +280,14 @@ let add_constant sp ce env =
 	  with NotConvertible -> 
 	    error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
   in
+  let ids = 
+    Idset.union (global_vars_set ce.const_entry_body) (global_vars_set ty.body)
+  in
   let cb = { 
     const_kind = kind_of_path sp;
     const_body = Some ce.const_entry_body;
     const_type = ty;
-    const_hyps = var_context env;
+    const_hyps = keep_hyps (var_context env) ids;
     const_constraints = Constraint.union cst cst';
     const_opaque = false } 
   in
@@ -293,11 +296,12 @@ let add_constant sp ce env =
 let add_parameter sp t env =
   let (jt,cst) = safe_machine env t in
   let env' = add_constraints cst env in
+  let ids = global_vars_set jt.uj_val in
   let cb = {
     const_kind = kind_of_path sp;
     const_body = None;
     const_type = assumption_of_judgment env' Evd.empty jt;
-    const_hyps = var_context env;
+    const_hyps = keep_hyps (var_context env) ids;
     const_constraints = cst;
     const_opaque = false } 
   in
@@ -333,7 +337,7 @@ let enforce_type_constructor env univ j cst =
     | _ -> error "Type of Constructor not well-formed"
 
 let type_one_constructor env_ar nparams ar c =
-  let (params,dc) = decompose_prod_n nparams c in
+  let (params,dc) = mind_extract_params nparams c in
   let env_par = push_rels params env_ar in
   let (jc,cst) = safe_machine env_par dc in
   let cst' = match sort_of_arity env_ar ar with
@@ -356,8 +360,10 @@ let logic_arity env c =
 let is_unit env_par nparams ar spec =
   match decomp_all_DLAMV_name spec with
     | (_,[|c|]) ->
-	(let (_,a) = decompose_prod_n nparams ar in logic_arity env_par ar) &&
-	(let (_,c') = decompose_prod_n nparams c in logic_constr env_par c')
+	(let (_,a) = mind_extract_params nparams ar in 
+	 logic_arity env_par ar) &&
+	(let (_,c') = mind_extract_params nparams c in 
+	 logic_constr env_par c')
     | _ -> false
 
 let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,spec) =
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 255e8d7aa..46dd75078 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -954,3 +954,19 @@ let control_only_guard env sigma =
     | DLAMV(_,v)    -> Array.iter control_rec v
   in 
   control_rec 
+
+(* [keep_hyps sign ids] keeps the part of the signature [sign] which 
+   contains the variables of the set [ids], and recursively the variables 
+   contained in the types of the needed variables. *)
+
+let keep_hyps sign needed =
+  rev_sign
+    (fst (it_sign 
+	    (fun ((hyps,globs) as sofar) id a ->
+               if Idset.mem id globs then
+                 (add_sign (id,a) hyps, 
+		  Idset.union (global_vars_set a.body) globs)
+               else 
+		 sofar) 
+	    (nil_sign,needed) sign))
+    
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 8a2974f6c..9542dba9f 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -90,3 +90,5 @@ val find_case_dep_nparams :
 val type_inst_construct : env -> 'a evar_map -> int -> constr -> constr 
 
 val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool
+
+val keep_hyps : var_context -> Idset.t -> var_context
diff --git a/lib/util.ml b/lib/util.ml
index 8410367f9..567c8edb6 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -231,6 +231,8 @@ let list_except_assoc e =
   in 
   except_e 
 
+let list_join_map f l = List.flatten (List.map f l)
+
 
 (* Arrays *)
 
diff --git a/lib/util.mli b/lib/util.mli
index e0de343df..e0743627d 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -72,6 +72,7 @@ val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
 val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
 val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
 val list_except_assoc : 'a -> ('a * 'b) list -> ('a * 'b) list
+val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
 
 
 (*s Arrays. *)
diff --git a/parsing/coqast.ml b/parsing/coqast.ml
index b0a825326..0f0dcda29 100644
--- a/parsing/coqast.ml
+++ b/parsing/coqast.ml
@@ -15,6 +15,22 @@ type t =
 
 type the_coq_ast = t
 
+let subst_meta bl ast =
+  let rec aux = function
+    | Node (_,"META", [Num(_, n)]) -> List.assoc n bl
+    | Node(loc, node_name, args) -> 
+	Node(loc, node_name, List.map aux args)
+    | Slam(loc, var, arg) -> Slam(loc, var, aux arg)
+    | other -> other
+  in 
+  aux ast
+
+let rec collect_metas = function
+  | Node (_,"META", [Num(_, n)]) -> [n]
+  | Node(_, _, args) -> List.concat (List.map collect_metas args)
+  | Slam(loc, var, arg) -> collect_metas arg
+  | _ -> []
+
 (* Hash-consing *)
 module Hloc = Hashcons.Make(
   struct
diff --git a/parsing/coqast.mli b/parsing/coqast.mli
index 006b98b3e..3a02092cd 100644
--- a/parsing/coqast.mli
+++ b/parsing/coqast.mli
@@ -1,6 +1,8 @@
 
 (* $Id$ *)
 
+(* Abstract syntax trees. *)
+
 type loc = int * int
 
 type t =
@@ -13,5 +15,13 @@ type t =
   | Path of loc * string list* string
   | Dynamic of loc * Dyn.t
 
+(* returns the list of metas occuring in the ast *)
+val collect_metas : t -> int list
+
+(* [subst_meta bl ast]: for each binding [(i,c_i)] in [bl], 
+   replace the metavar [?i] by [c_i] in [ast] *)
+val subst_meta : (int * t) list -> t -> t
+
+(* hash-consing function *)
 val hcons_ast: (string -> string) -> (t -> t) * (loc -> loc)
 
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 3413b2a61..9e6f3006e 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -154,3 +154,7 @@ let vernac_interp_atomic =
 	 | _ -> assert false)
   in 
   fun opn args -> gentac ((Identifier opn)::args)
+
+let bad_tactic_args s =
+  anomalylabstrm s
+    [< 'sTR"Tactic "; 'sTR s; 'sTR" called with bad arguments" >]
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index aa71f411d..3e913f808 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -24,3 +24,5 @@ val vernac_interp_atomic : identifier -> tactic_arg list -> tactic
 val overwriting_tacinterp_add : string * (tactic_arg list -> tactic) -> unit
 val is_just_undef_macro     : Coqast.t -> string option
 
+val bad_tactic_args : string -> 'a
+
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 2dc69c55b..6358366b7 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -22,6 +22,7 @@ open Hiddentac
 open Libobject
 open Library
 open Vernacinterp
+open Printer
 
 (****************************************************************************)
 (*            The Type of Constructions Autotactic Hints                    *)
@@ -33,7 +34,7 @@ type auto_tactic =
   | 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 *) 
+  | Extern of Coqast.t                   (* Hint Extern *) 
 
 type pri_auto_tactic = { 
   hname : identifier;    (* name of the hint *)
@@ -120,9 +121,9 @@ end
 
 type frozen_hint_db_table = Hint_db.t Stringmap.t 
 
-type hint_db_table = Hint_db.t Stringmap.t
+type hint_db_table = Hint_db.t Stringmap.t ref
 
-let searchtable  = ref (Stringmap.empty : hint_db_table)
+let searchtable = (ref Stringmap.empty : hint_db_table)
 
 let searchtable_map name = 
   Stringmap.find name !searchtable
@@ -190,7 +191,7 @@ let make_exact_entry name (c,cty) =
 	 { hname=name; pri=0; pat=None; code=Give_exact c })
 
 let make_apply_entry (eapply,verbose) name (c,cty) =
-  match hnf_constr (Global.unsafe_env()) Evd.empty cty with
+  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
@@ -227,7 +228,7 @@ let make_resolves name eap (c,cty) =
       [make_exact_entry; make_apply_entry eap]
   in 
   if ents = [] then 
-    errorlabstrm "Hint" [< pTERM c; 'sPC; 'sTR "cannot be used as a hint" >];
+    errorlabstrm "Hint" [< prterm c; 'sPC; 'sTR "cannot be used as a hint" >];
   ents
 
 (* used to add an hypothesis to the local hint database *)
@@ -246,7 +247,7 @@ let add_resolves clist dbnames =
 	    (dbname,
      	     (List.flatten
 		(List.map (fun (name,c) -> 
-			     let env = Global.unsafe_env() in
+			     let env = Global.env() in
 			     let ty = type_of env Evd.empty c in
 			     make_resolves name (true,true) (c,ty)) clist))
 	    )))
@@ -284,21 +285,21 @@ let make_extern name pri pat tacast =
 let add_extern name pri 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 tacmetas = Coqast.collect_metas tacast in 
   let patmetas = Clenv.collect_metas pat in
-  match (subtract tacmetas patmetas) with
+  match (list_subtract tacmetas patmetas) with
     | i::_ ->
 	errorlabstrm "add_extern" 
 	  [< 'sTR "The meta-variable ?"; 'iNT i; 'sTR" is not bound" >]
     | []  ->
-	add_anonymous_object 
+	Lib.add_anonymous_leaf
 	  (inAutoHint(dbname, [make_extern name pri pat tacast]))
 
 let add_externs name pri pat tacast dbnames = 
   List.iter (add_extern name pri pat tacast) dbnames
 
 let make_trivial (name,c) =
-  let sigma = Evd.empty and env = Global.unsafe_env() in
+  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 ce = mk_clenv_from () (c,hnf_constr env sigma t) in
@@ -329,7 +330,7 @@ let _ =
     "HintResolve"
     (function 
        | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_COMMAND c] ->
-	   let c1 = Trad.constr_of_com (Evd.mt_evd()) (initial_sign()) c in
+	   let c1 = Astterm.constr_of_com Evd.empty (Global.env()) c in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function VARG_IDENTIFIER i -> string_of_id i
 		      	 | _ -> bad_vernac_args "HintResolve") l in
@@ -341,7 +342,7 @@ let _ =
     "HintImmediate"
     (function 
        | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_COMMAND c] ->
-	   let c1 = Trad.constr_of_com (Evd.mt_evd()) (initial_sign()) c in
+	   let c1 = Astterm.constr_of_com Evd.empty (Global.env()) c in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function VARG_IDENTIFIER i -> string_of_id i
 			 | _ -> bad_vernac_args "HintImmediate") l in
@@ -377,7 +378,7 @@ let _ =
        | [VARG_IDENTIFIER hintname; VARG_VARGLIST l;
 	  VARG_NUMBER pri; VARG_COMMAND patcom; VARG_TACTIC tacexp] ->
            let pat = Pattern.raw_sopattern_of_compattern 
-		       (initial_sign()) patcom in
+		       (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
@@ -507,7 +508,7 @@ let fmt_hint_term cl =
 		      'sTR " :"; 'fNL;
 		      fmt_hint_list hintlist >])
 	   valid_dbs >]
-  with BOUND | Match_failure _ | Failure _ -> 
+  with Bound | Match_failure _ | Failure _ -> 
     [<'sTR "No hint applicable for current goal" >]
 	  
 let print_hint_term cl = pPNL (fmt_hint_term cl)
@@ -542,29 +543,29 @@ let print_searchtable () =
     !searchtable
 
 let _ = 
-  vinterp_add("PrintHint",
-	      function 
-		| [] -> fun () -> print_searchtable()
-	        | _ -> assert false)
+  vinterp_add "PrintHint"
+    (function 
+       | [] -> fun () -> print_searchtable()
+       | _ -> bad_vernac_args "PrintHint")
 
 let _ = 
-  vinterp_add("PrintHintDb",
-	      function 
-	      	| [(VARG_IDENTIFIER id)] -> 
-		    fun () -> print_hint_db_by_name (string_of_id id)
-	      	| _ -> assert false)
+  vinterp_add "PrintHintDb"
+    (function 
+       | [(VARG_IDENTIFIER id)] -> 
+	   fun () -> print_hint_db_by_name (string_of_id id)
+       | _ -> bad_vernac_args "PrintHintDb")
 
 let _ = 
-  vinterp_add("PrintHintGoal",
-	      function 
-		| [] -> fun () -> print_applicable_hint()
-	        | _ -> assert false)
+  vinterp_add "PrintHintGoal"
+    (function 
+       | [] -> fun () -> print_applicable_hint()
+       | _ -> bad_vernac_args "PrintHintGoal")
     
 let _ = 
-  vinterp_add("PrintHintId",
-	      function 
-		| [(VARG_IDENTIFIER id)] -> fun () -> print_hint_id id
-	        | _ -> assert false)
+  vinterp_add "PrintHintId"
+    (function 
+       | [(VARG_IDENTIFIER id)] -> fun () -> print_hint_id id
+       | _ -> bad_vernac_args "PrintHintId")
 
 (**************************************************************************)
 (*                           Automatic tactics                            *)
@@ -635,7 +636,7 @@ and my_find_search db_list local_db hdc concl =
 		(trivial_fail_db db_list local_db)
 	  | Unfold_nth c -> unfold_constr c
 	  | Extern tacast -> 
-	      conclPattern concl (outSOME p) tacast))
+	      conclPattern concl (out_some p) tacast))
     tacl
 
 and trivial_resolve db_list local_db cl = 
@@ -888,7 +889,7 @@ let search_superauto n ids argl g =
     ids,
     (List.map (fun id -> pf_type_of g (pf_global g id)) ids) in   
   let hyps = (concat_sign (pf_untyped_hyps g) sigma) in
-  super_search n [Fmavm.map searchtable "core"] (make_local_hint_db hyps)
+  super_search n [Stringmap.find "core" !searchtable] (make_local_hint_db hyps)
     argl g
 
 let superauto n ids_add argl  = 
@@ -907,13 +908,13 @@ let dyn_superauto l g =
   match l with
     | (Integer n)::(Clause ids_add)::l -> 
         superauto n ids_add 
-          (join_map_list 
+          (list_join_map
              (function 
 		| Quoted_string s -> (cvt_autoArgs s)
                 | _ -> assert false) l) g
     | _::(Clause ids_add)::l  -> 
         superauto !default_search_depth ids_add 
-          (join_map_list 
+          (list_join_map
              (function 
 		| Quoted_string s -> (cvt_autoArgs s)
                 | _ -> assert false) l) g
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 333aca134..82a8ee792 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -44,7 +44,7 @@ module Hint_db :
 
 type frozen_hint_db_table = Hint_db.t Stringmap.t
 
-type hint_db_table = Hint_db.t Stringmap.t
+type hint_db_table = Hint_db.t Stringmap.t ref
 
 val searchtable : hint_db_table
 
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index e4d79051c..6efa9c686 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -109,6 +109,7 @@ open Util
 open Names
 open Generic
 open Term
+open Environ
 open Reduction
 open Proof_trees
 open Tacmach
@@ -120,6 +121,9 @@ open Libobject
 open Library
 open Vernacinterp
 open Pattern
+open Coqast
+open Ast
+open Pcoq
 
 (* two patterns - one for the type, and one for the type of the type *)
 type destructor_pattern = {
@@ -200,28 +204,29 @@ let add_destructor_hint na pat pri code =
     (inDD (na,{ d_pat = pat; d_pri=pri; d_code=code }))
 
 let _ = 
-  vinterp_add
-    ("HintDestruct",
-     fun [VARG_IDENTIFIER na; VARG_AST location; VARG_COMMAND patcom;
+  vinterp_add "HintDestruct"
+    (function
+       | [VARG_IDENTIFIER na; VARG_AST location; VARG_COMMAND patcom;
           VARG_NUMBER pri; VARG_AST tacexp] ->
-       let loc =
-	 match location with
-           | Node(_,"CONCL",[]) -> CONCL()
-	   | Node(_,"DiscardableHYP",[]) -> HYP true
-	   | Node(_,"PreciousHYP",[]) -> HYP false 
-       in
-       fun () ->
-	 let pat = raw_sopattern_of_compattern (initial_sign()) 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(newMETA()))},
-                      { d_typ=DOP0(Meta(newMETA()));
-		       	d_sort=DOP0(Meta(newMETA())) })
-              | CONCL () ->
-		  CONCL({d_typ=pat;d_sort=DOP0(Meta(newMETA()))}))
-           pri code)
+	   let loc = match location with
+             | Node(_,"CONCL",[]) -> Concl()
+	     | Node(_,"DiscardableHYP",[]) -> Hyp true
+	     | Node(_,"PreciousHYP",[]) -> Hyp false 
+	     | _ -> assert false
+	   in
+	   fun () ->
+	     let pat = raw_sopattern_of_compattern (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())) })
+		  | Concl () ->
+		      Concl({d_typ=pat;d_sort=DOP0(Meta(new_meta()))}))
+               pri code
+       | _ -> bad_vernac_args "HintDestruct")
 
 let match_dpat dp cls gls =
   let cltyp = clause_type cls gls in
@@ -242,12 +247,15 @@ let applyDestructor cls discard dd gls =
     | Some id -> ["$0", Vast (nvar (string_of_id id))]
     | None -> ["$0", Vast (nvar "$0")] in
   (* TODO: find the real location *)
-  let (Vast tcom) = Ast.eval_act dummy_loc astb dd.d_code in
+  let tcom = match Ast.eval_act dummy_loc astb dd.d_code with
+    | Vast tcom -> tcom
+    | _ -> assert false 
+  in
   let discard_0 =
     match (cls,dd.d_pat) with
-      | (Some id,HYP(discardable,_,_)) ->
+      | (Some id,Hyp(discardable,_,_)) ->
           if discard & discardable then thin [id] else tclIDTAC
-      | (None,CONCL _) -> tclIDTAC
+      | (None,Concl _) -> tclIDTAC
       | _ -> error "ApplyDestructor" 
   in
   (tclTHEN (Tacinterp.interp tcom) discard_0) gls
@@ -269,8 +277,17 @@ let dHyp id gls = destructHyp false id gls
 
 open Tacinterp
 
-let _ = tacinterp_add("DHyp",(fun [Identifier id] -> dHyp id))
-let _ = tacinterp_add("CDHyp",(fun [Identifier id] -> cDHyp id))
+let _ = 
+  tacinterp_add
+    ("DHyp",(function
+	       | [Identifier id] -> dHyp id
+	       | _ -> bad_tactic_args "DHyp"))
+
+let _ = 
+  tacinterp_add
+    ("CDHyp",(function
+		| [Identifier id] -> cDHyp id
+		| _ -> bad_tactic_args "CDHyp"))
 
 (* [DConcl gls]
 
@@ -283,9 +300,13 @@ let dConcl gls =
   let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
   tclFIRST (List.map (applyDestructor None false) sorted_ddl) gls
 
-let _ = tacinterp_add("DConcl",(fun [] -> dConcl))
+let _ = 
+  tacinterp_add
+    ("DConcl",(function
+		 | [] -> dConcl
+		 | _ -> bad_tactic_args "DConcl"))
 
-let to2Lists (table:t) = Nbtermdn.to2Lists table
+let to2Lists (table:t) = Nbtermdn.to2lists table
 
 let rec search n =
   if n=0 then error "Search has reached zero.";
@@ -306,5 +327,6 @@ let sarch_depth_tdb = ref(5)
 let dyn_auto_tdb = function 
   | [Integer n] -> auto_tdb n 
   | []          -> auto_tdb !sarch_depth_tdb
+  | _           -> bad_tactic_args "AutoTDB"
 
 let h_auto_tdb = hide_tactic "AutoTDB" dyn_auto_tdb
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index b59df6334..de81cce91 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.mli
@@ -1,5 +1,12 @@
 
 (* $Id$ *)
 
+(*i*)
+open Names
+open Tacmach
+(*i*)
+
 (* Programmable destruction of hypotheses and conclusions. *)
 
+val dHyp : identifier -> tactic
+val dConcl : tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index ff5d324a3..bae9c8798 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -191,7 +191,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 = 
@@ -199,8 +199,7 @@ let conclPattern concl pat tacast gl =
       (fun (i,c) -> (i, Termast.bdize false (assumptions_for_print []) c))
       constr_bindings in 
   let tacast' = Coqast.subst_meta ast_bindings tacast in
-    Tacinterp.interp tacast' gl
-***)
+  Tacinterp.interp tacast' gl
 
 let clauseTacThen tac continuation =
   (fun cls -> (tclTHEN (tac cls) continuation))
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 298b5abd9..49acb49e4 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -77,9 +77,8 @@ val ifOnClause     :
    if the term concl matches the pattern pat, (in sense of 
    Pattern.somatches, then replace ?1 ?2 metavars in tacast by the
    right values to build a tactic *)
-(***
-val conclPattern : constr -> constr -> CoqAst.t -> tactic
-**i*)
+
+val conclPattern : constr -> constr -> Coqast.t -> tactic
 
 (*s Elimination tacticals. *)