Integrating the Ltac language and the Blast tool into the interface

capabilities:

The Ltac language is the language that makes it possible to define new tactics
without using the ocaml language (already present in coq for a few months).

The Blast tool is a tool that checks whether the goals could be solve
automatically and proposes the proof trace to the user.


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

10 files changed, 1039 insertions, 292 deletions

diff --git a/contrib/interface/Centaur.v b/contrib/interface/Centaur.v
index 5cca616a53..654cf123fa 100644
--- a/contrib/interface/Centaur.v
+++ b/contrib/interface/Centaur.v
@@ -5,6 +5,7 @@ Declare ML Module "xlate".
 Declare ML Module "vtp".
 Declare ML Module "translate".
 Declare ML Module "pbp".
+Declare ML Module "blast".
 Declare ML Module "dad".
 Declare ML Module "showproof_ct".
 Declare ML Module "showproof".
@@ -55,6 +56,8 @@ Grammar tactic simple_tactic : ast :=
 | pbp2 [ "Pbp" identarg($id) ] -> [ (PcoqPbp $id) ]
 | pbp3 [ "Pbp" identarg($id) ne_num_list($ns)] ->
          [ (PcoqPbp $id ($LIST $ns)) ]
+| blast1 [ "Blast" ne_num_list($ns) ] ->
+         [ (PcoqBlast ($LIST $ns)) ]
 | dad00 [ "Dad" "to" ] -> [(Dad (TACTIC (to)))]
 | dad01 [ "Dad" "to" ne_num_list($ns) ] ->
         [(Dad (TACTIC (to)) ($LIST $ns))]
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 3b9d742e26..4527f66086 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -1,4 +1,3 @@
-
 type ct_ASSOC =
     CT_coerce_NONE_to_ASSOC of ct_NONE
   | CT_lefta
@@ -169,7 +168,9 @@ and ct_CONTEXT_RULE =
 and ct_CONVERSION_FLAG =
     CT_beta
   | CT_delta
+  | CT_evar
   | CT_iota
+  | CT_zeta
 and ct_CONVERSION_FLAG_LIST =
     CT_conversion_flag_list of ct_CONVERSION_FLAG list
 and ct_CONV_SET =
@@ -183,8 +184,8 @@ and ct_DEFN_OR_THM =
     CT_coerce_DEFN_to_DEFN_OR_THM of ct_DEFN
   | CT_coerce_THM_to_DEFN_OR_THM of ct_THM
 and ct_DEF_BODY =
-    CT_coerce_EVAL_CMD_to_DEF_BODY of ct_EVAL_CMD
-  | CT_coerce_FORMULA_to_DEF_BODY of ct_FORMULA
+    CT_coerce_CONTEXT_PATTERN_to_DEF_BODY of ct_CONTEXT_PATTERN
+  | CT_coerce_EVAL_CMD_to_DEF_BODY of ct_EVAL_CMD
 and ct_DEP =
     CT_dep of string
 and ct_DESTRUCTING =
@@ -226,7 +227,6 @@ and ct_FORMULA =
   | CT_int_encapsulator of ct_INT
   | CT_lambdac of ct_BINDER * ct_FORMULA
   | CT_letin of ct_ID * ct_FORMULA * ct_FORMULA
-  | CT_metac of ct_INT
   | CT_prodc of ct_BINDER * ct_FORMULA
 and ct_FORMULA_LIST =
     CT_formula_list of ct_FORMULA list
@@ -245,6 +245,7 @@ and ct_HINT_EXPRESSION =
   | CT_unfold_hint of ct_ID
 and ct_ID =
     CT_ident of string
+  | CT_metac of ct_INT
 and ct_IDENTITY_OPT =
     CT_coerce_NONE_to_IDENTITY_OPT of ct_NONE
   | CT_identity
@@ -307,6 +308,13 @@ and ct_IN_OR_OUT_MODULES =
     CT_coerce_NONE_to_IN_OR_OUT_MODULES of ct_NONE
   | CT_in_modules of ct_ID_NE_LIST
   | CT_out_modules of ct_ID_NE_LIST
+and ct_LET_CLAUSE =
+    CT_let_clause of ct_ID * ct_LET_VALUE
+and ct_LET_CLAUSES =
+    CT_let_clauses of ct_LET_CLAUSE * ct_LET_CLAUSE list
+and ct_LET_VALUE =
+    CT_coerce_DEF_BODY_to_LET_VALUE of ct_DEF_BODY
+  | CT_coerce_TACTIC_COM_to_LET_VALUE of ct_TACTIC_COM
 and ct_LOCAL_OPT =
     CT_coerce_NONE_to_LOCAL_OPT of ct_NONE
   | CT_local
@@ -318,6 +326,10 @@ and ct_MATCH_PATTERN =
   | CT_pattern_as of ct_MATCH_PATTERN * ct_ID_OPT
 and ct_MATCH_PATTERN_NE_LIST =
     CT_match_pattern_ne_list of ct_MATCH_PATTERN * ct_MATCH_PATTERN list
+and ct_MATCH_TAC_RULE =
+    CT_match_tac_rule of ct_CONTEXT_PATTERN * ct_LET_VALUE
+and ct_MATCH_TAC_RULES =
+    CT_match_tac_rules of ct_MATCH_TAC_RULE * ct_MATCH_TAC_RULE list
 and ct_NATURAL_FEATURE =
     CT_contractible
   | CT_implicit
@@ -460,8 +472,9 @@ and ct_TACTIC_COM =
   | CT_intros_until of ct_ID
   | CT_inversion of ct_INV_TYPE * ct_ID * ct_ID_LIST
   | CT_left of ct_SPEC_LIST
-  | CT_lettac of ct_ID * ct_FORMULA * ct_UNFOLD_NE_LIST
+  | CT_lettac of ct_LET_CLAUSES * ct_LET_VALUE
   | CT_match_context of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
+  | CT_match_tac of ct_LET_VALUE * ct_MATCH_TAC_RULES
   | CT_move_after of ct_ID * ct_ID
   | CT_omega
   | CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
new file mode 100755
index 0000000000..104051b2d1
--- /dev/null
+++ b/contrib/interface/blast.ml
@@ -0,0 +1,627 @@
+(* Une tactique qui tente de démontrer toute seule le but courant,
+   interruptible par pcoq (si dans le fichier C:\WINDOWS\free il y a un A)
+*)
+open Ctast;;
+open Termops;;
+open Nameops;;
+open Astterm;;
+open Auto;;
+open Clenv;;
+open Command;;
+open Ctast;;
+open Declarations;;
+open Declare;;
+open Eauto;;
+open Environ;;
+open Equality;;
+open Evd;;
+open Hipattern;;
+open Inductive;;
+open Names;;
+open Pattern;;
+open Pbp;;
+open Pfedit;;
+open Pp;;
+open Printer
+open Proof_trees;;
+open Proof_type;;
+open Rawterm;;
+open Reduction;;
+open Refiner;;
+open Sign;;
+open String;;
+open Tacmach;;
+open Tacred;;
+open Tacticals;;
+open Tactics;;
+open Term;;
+open Typing;;
+open Util;;
+open Vernacentries;;
+open Vernacinterp;;
+open Evar_refiner;;
+
+
+let parse_com   = Pcoq.parse_string Pcoq.Constr.constr;;
+let parse_tac  t =
+    try (Pcoq.parse_string Pcoq.Tactic.tactic t)
+    with _ -> (msgnl (hov 0 (str"pas parsé: " ++ str t));
+	       failwith "tactic")
+;;
+
+let is_free () =
+   let st =open_in_bin ((Sys.getenv "HOME")^"/.free") in
+   let c=input_char st in
+   close_in st;
+   c = 'A'
+;;
+
+(* marche pas *)
+(*
+let is_free () =
+   msgnl (hov 0 [< 'str"Isfree========= "; 'fNL >]);
+   let s = Stream.of_channel stdin in
+   msgnl (hov 0 [< 'str"Isfree s "; 'fNL >]);
+   try (Stream.empty s;
+        msgnl (hov 0 [< 'str"Isfree empty "; 'fNL >]);
+        true)
+   with _ -> (msgnl (hov 0 [< 'str"Isfree not empty "; 'fNL >]);
+              false)
+;;
+*)
+let free_try tac g =
+    if is_free()
+    then (tac g)
+    else (failwith "not free")
+;;
+let adrel (x,t) e =
+    match x with 
+      Name(xid) -> Environ.push_rel (x,None,t) e
+    | Anonymous -> Environ.push_rel (x,None,t) e
+(* les constantes ayant une définition apparaissant dans x *)
+let rec def_const_in_term_rec vl x = 
+     match (kind_of_term x) with
+     Prod(n,t,c)->
+        let vl = (adrel (n,t) vl) in def_const_in_term_rec vl c
+   | Lambda(n,t,c) ->
+        let vl = (adrel (n,t) vl) in def_const_in_term_rec vl c
+   | App(f,args) -> def_const_in_term_rec vl f
+   | Sort(Prop(Null)) -> Prop(Null)
+   | Sort(c) -> c
+   | Ind(ind) ->
+          let (mib, mip) = Global.lookup_inductive ind in
+          mip.mind_sort
+   | Construct(c) ->
+          def_const_in_term_rec vl (mkInd (inductive_of_constructor c))
+   | Case(_,x,t,a) 
+        -> def_const_in_term_rec vl x
+   | Cast(x,t)-> def_const_in_term_rec vl t
+   | Const(c)  -> def_const_in_term_rec vl (lookup_constant c vl).const_type
+   | _ -> def_const_in_term_rec vl (type_of vl Evd.empty x)
+;;
+let def_const_in_term_ x =
+    def_const_in_term_rec  (Global.env()) (strip_outer_cast x)
+;;
+(*************************************************************************
+ recopiés de refiner.ml, car print_subscript pas exportée dans refiner.mli 
+ modif de print_info_script avec pr_bar
+*)
+
+let pr_bar () = str "|"
+
+let rec print_info_script sigma osign pf =
+  let {evar_hyps=sign; evar_concl=cl} = pf.goal in
+  match pf.ref with
+    | None -> [< >]
+    | Some(r,spfl) ->
+        pr_rule r ++
+           match spfl with
+             | [] ->
+		   (str " " ++ fnl())
+             | [pf1] ->
+                 if pf1.ref = None then 
+		   (str " " ++ fnl())
+                 else 
+		   (str";" ++ brk(1,3) ++
+		      print_info_script sigma sign pf1)
+             | _ -> ( str";[" ++ fnl() ++
+                       prlist_with_sep pr_bar
+                         (print_info_script sigma sign) spfl ++
+                       str"]")
+
+let format_print_info_script sigma osign pf = 
+  hov 0 (print_info_script sigma osign pf)
+    
+let print_subscript sigma sign pf = 
+ (* if is_tactic_proof pf then 
+    format_print_info_script sigma sign (subproof_of_proof pf)
+  else *)
+    format_print_info_script sigma sign pf
+(****************)
+
+let pp_string x =
+   msgnl_with Format.str_formatter x;
+   Format.flush_str_formatter ()
+;;
+
+(***********************************************************************
+   copié de tactics/eauto.ml
+*)
+
+(***************************************************************************)
+(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
+(***************************************************************************)
+
+let unify_e_resolve  (c,clenv) gls = 
+  let (wc,kONT) = startWalk gls in
+  let clenv' = connect_clenv wc clenv in
+  let _ = clenv_unique_resolver false clenv' gls in
+  vernac_e_resolve_constr c gls
+
+let rec e_trivial_fail_db db_list local_db goal =
+  let tacl = 
+    registered_e_assumption ::
+    (tclTHEN Tactics.intro 
+       (function g'->
+	  let d = pf_last_hyp g' in
+	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
+          (e_trivial_fail_db db_list
+	     (Hint_db.add_list hintl local_db) g'))) ::
+    (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
+  in 
+  tclFIRST (List.map tclCOMPLETE tacl) goal 
+
+and e_my_find_search db_list local_db hdc concl = 
+  let hdc = head_of_constr_reference hdc in
+  let hintl =
+    if occur_existential concl then 
+      list_map_append (Hint_db.map_all hdc) (local_db::db_list)
+    else 
+      list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
+  in 
+  let tac_of_hint = 
+    fun ({pri=b; pat = p; code=t} as patac) -> 
+      (b, 
+       let tac =
+	 match t with
+	   | Res_pf (term,cl) -> unify_resolve (term,cl)
+	   | ERes_pf (term,cl) -> unify_e_resolve (term,cl)
+	   | Give_exact (c) -> e_give_exact_constr c
+	   | Res_pf_THEN_trivial_fail (term,cl) ->
+               tclTHEN (unify_e_resolve (term,cl)) 
+		 (e_trivial_fail_db db_list local_db)
+	   | Unfold_nth c -> unfold_constr c
+	   | Extern tacast -> Tacticals.conclPattern concl 
+	       (out_some p) tacast
+       in 
+       (free_try tac,fmt_autotactic t))
+       (*i
+	 fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); 
+                     try tac gls
+		     with e when Logic.catchable_exception(e) -> 
+                            (Format.print_string "Fail\n"; 
+			     Format.print_flush (); 
+			     raise e)
+       i*)
+  in 
+  List.map tac_of_hint hintl
+    
+and e_trivial_resolve db_list local_db gl = 
+  try 
+    Auto.priority 
+      (e_my_find_search db_list local_db 
+	 (List.hd (head_constr_bound gl [])) gl)
+  with Bound | Not_found -> []
+
+let e_possible_resolve db_list local_db gl =
+  try List.map snd (e_my_find_search db_list local_db 
+		      (List.hd (head_constr_bound gl [])) gl)
+  with Bound | Not_found -> []
+
+let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
+
+let find_first_goal gls = 
+  try first_goal gls with UserError _ -> assert false
+
+(*s The following module [SearchProblem] is used to instantiate the generic
+    exploration functor [Explore.Make]. *)
+      
+module MySearchProblem = struct
+
+  type state = { 
+    depth : int; (*r depth of search before failing *)
+    tacres : goal list sigma * validation;
+    last_tactic : std_ppcmds;
+    dblist : Auto.Hint_db.t list;
+    localdb :  Auto.Hint_db.t list }
+		 
+  let success s = (sig_it (fst s.tacres)) = []
+
+  let rec filter_tactics (glls,v) = function
+    | [] -> []
+    | (tac,pptac) :: tacl -> 
+	try 
+	  let (lgls,ptl) = apply_tac_list tac glls in 
+	  let v' p = v (ptl p) in
+	  ((lgls,v'),pptac) :: filter_tactics (glls,v) tacl
+	with e when Logic.catchable_exception e ->
+	  filter_tactics (glls,v) tacl
+
+  let rec list_addn n x l = 
+    if n = 0 then l else x :: (list_addn (pred n) x l)
+
+  (* Ordering of states is lexicographic on depth (greatest first) then
+     number of remaining goals. *)
+  let compare s s' =
+    let d = s'.depth - s.depth in
+    let nbgoals s = List.length (sig_it (fst s.tacres)) in
+    if d <> 0 then d else nbgoals s - nbgoals s'
+
+  let branching s = 
+    if s.depth = 0 then 
+      []
+    else      
+      let lg = fst s.tacres in
+      let nbgl = List.length (sig_it lg) in
+      assert (nbgl > 0);
+      let g = find_first_goal lg in
+      let assumption_tacs = 
+	let l = 
+	  filter_tactics s.tacres
+	    (List.map 
+	       (fun id -> (e_give_exact_constr (mkVar id),
+			   (str "Exact" ++ spc()++ pr_id id)))
+	       (pf_ids_of_hyps g))
+	in
+	List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
+				    last_tactic = pp; dblist = s.dblist;
+				    localdb = List.tl s.localdb }) l
+      in
+      let intro_tac = 
+	List.map 
+	  (fun ((lgls,_) as res,pp) -> 
+	     let g' = first_goal lgls in 
+	     let hintl = 
+	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
+	     in
+             let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
+	     { depth = s.depth; tacres = res; 
+	       last_tactic = pp; dblist = s.dblist;
+	       localdb = ldb :: List.tl s.localdb })
+	  (filter_tactics s.tacres [Tactics.intro,(str "Intro" )])
+      in
+      let rec_tacs = 
+	let l = 
+	  filter_tactics s.tacres
+	    (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
+	in
+	List.map 
+	  (fun ((lgls,_) as res, pp) -> 
+	     let nbgl' = List.length (sig_it lgls) in
+	     if nbgl' < nbgl then
+	       { depth = s.depth; tacres = res; last_tactic = pp;
+		 dblist = s.dblist; localdb = List.tl s.localdb }
+	     else 
+	       { depth = pred s.depth; tacres = res; 
+		 dblist = s.dblist; last_tactic = pp;
+		 localdb = 
+		   list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
+	  l
+      in
+      List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
+
+  let pp s = 
+    msg (hov 0 (str " depth="++ int s.depth ++ spc() ++
+		  s.last_tactic ++ str "\n"))
+
+end
+
+module MySearch = Explore.Make(MySearchProblem)
+
+let make_initial_state n gl dblist localdb =
+  { MySearchProblem.depth = n;
+    MySearchProblem.tacres = tclIDTAC gl;
+    MySearchProblem.last_tactic = [< >];
+    MySearchProblem.dblist = dblist;
+    MySearchProblem.localdb = [localdb] }
+
+let e_depth_search debug p db_list local_db gl =
+  try
+    let tac = if debug then MySearch.debug_depth_first else MySearch.depth_first in
+    let s = tac (make_initial_state p gl db_list local_db) in
+    s.MySearchProblem.tacres
+  with Not_found -> error "EAuto: depth first search failed"
+
+let e_breadth_search debug n db_list local_db gl =
+  try
+    let tac = 
+      if debug then MySearch.debug_breadth_first else MySearch.breadth_first 
+    in
+    let s = tac (make_initial_state n gl db_list local_db) in
+    s.MySearchProblem.tacres
+  with Not_found -> error "EAuto: breadth first search failed"
+
+let e_search_auto debug (n,p) db_list gl = 
+  let local_db = make_local_hint_db gl in 
+  if n = 0 then 
+    e_depth_search debug p db_list local_db gl
+  else 
+    e_breadth_search debug n db_list local_db gl
+
+let eauto debug np dbnames = 
+  let db_list =
+    List.map
+      (fun x -> 
+	 try Stringmap.find x !searchtable
+	 with Not_found -> error ("EAuto: "^x^": No such Hint database"))
+      ("core"::dbnames) 
+  in
+  tclTRY (e_search_auto debug np db_list)
+
+let full_eauto debug n gl = 
+  let dbnames = stringmap_dom !searchtable in
+  let dbnames =  list_subtract dbnames ["v62"] in
+  let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
+  let local_db = make_local_hint_db gl in
+  tclTRY (e_search_auto debug n db_list) gl
+
+let my_full_eauto n gl = full_eauto false (n,0) gl
+
+(**********************************************************************
+   copié de tactics/auto.ml on a juste modifié search_gen
+*)
+let searchtable_map name = 
+  Stringmap.find name !searchtable
+
+(* local_db is a Hint database containing the hypotheses of current goal *)
+(* Papageno : cette fonction a été pas mal simplifiée depuis que la base
+  de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
+
+let rec trivial_fail_db db_list local_db gl =
+  let intro_tac = 
+    tclTHEN intro 
+      (fun g'->
+	 let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
+	 in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g')
+  in
+  tclFIRST 
+    (assumption::intro_tac::
+     (List.map tclCOMPLETE 
+	(trivial_resolve db_list local_db (pf_concl gl)))) gl
+
+and my_find_search db_list local_db hdc concl =
+  let tacl = 
+    if occur_existential concl then 
+      list_map_append (fun db -> Hint_db.map_all hdc db) (local_db::db_list)
+    else 
+      list_map_append (fun db -> Hint_db.map_auto (hdc,concl) db)
+      	(local_db::db_list)
+  in
+  List.map 
+    (fun ({pri=b; pat=p; code=t} as patac) -> 
+       (b,
+	match t with
+	  | Res_pf (term,cl)  -> unify_resolve (term,cl)
+	  | ERes_pf (_,c) -> (fun gl -> error "eres_pf")
+	  | Give_exact c  -> exact_no_check c
+	  | Res_pf_THEN_trivial_fail (term,cl) -> 
+	      tclTHEN 
+		(unify_resolve (term,cl)) 
+		(trivial_fail_db db_list local_db)
+	  | Unfold_nth c -> unfold_constr c
+	  | Extern tacast -> 
+	      conclPattern concl (out_some p) tacast))
+    tacl
+
+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 (head_of_constr_reference hdconstr) cl)
+  with Bound | Not_found -> 
+    []
+
+(**************************************************************************)
+(*                       The classical Auto tactic                        *)
+(**************************************************************************)
+
+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 (head_of_constr_reference hdconstr) cl)
+  with Bound | Not_found -> 
+    []
+
+let decomp_unary_term c gls = 
+  let typc = pf_type_of gls c in 
+  let hd = List.hd (head_constr typc) in 
+  if Hipattern.is_conjunction hd then 
+    simplest_case c gls 
+  else 
+    errorlabstrm "Auto.decomp_unary_term" (str "not a unary type")
+
+let decomp_empty_term c gls = 
+  let typc = pf_type_of gls c in 
+  let (hd,_) = decompose_app typc in 
+  if Hipattern.is_empty_type hd then 
+    simplest_case c gls 
+  else 
+    errorlabstrm "Auto.decomp_empty_term" (str "not an empty type")
+
+
+(* decomp is an natural number giving an indication on decomposition 
+   of conjunction in hypotheses, 0 corresponds to no decomposition *)
+(* n is the max depth of search *)
+(* local_db contains the local Hypotheses *)
+
+let rec search_gen decomp n db_list local_db extra_sign goal =
+  if n=0 then error "BOUND 2";
+  let decomp_tacs = match decomp with 
+    | 0 -> [] 
+    | p -> 
+	(tclTRY_sign decomp_empty_term extra_sign)
+	::
+	(List.map 
+	   (fun id -> tclTHEN (decomp_unary_term (mkVar id)) 
+		(tclTHEN 
+		   (clear_one id)
+		   (free_try (search_gen decomp p db_list local_db []))))
+	   (pf_ids_of_hyps goal)) 
+  in
+  let intro_tac = 
+    tclTHEN intro 
+      (fun g' -> 
+	 let (hid,_,htyp as d) = pf_last_hyp g' in
+	 let hintl = 
+	   try 
+	     [make_apply_entry (pf_env g') (project g')
+		(true,false) 
+		hid (mkVar hid,body_of_type htyp)]
+	   with Failure _ -> [] 
+	 in
+         (free_try
+	  (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d])
+	  g'))
+  in
+  let rec_tacs = 
+    List.map 
+      (fun ntac -> 
+	 tclTHEN ntac
+	   (free_try
+	    (search_gen decomp (n-1) db_list local_db empty_named_context)))
+      (possible_resolve db_list local_db (pf_concl goal))
+  in 
+  tclFIRST (assumption::(decomp_tacs@(intro_tac::rec_tacs))) goal
+
+
+let search = search_gen 0
+
+let default_search_depth = ref 5
+			     
+let full_auto n gl = 
+  let dbnames = stringmap_dom !searchtable in
+  let dbnames = list_subtract dbnames ["v62"] in
+  let db_list = List.map (fun x -> searchtable_map x) dbnames in
+  let hyps = pf_hyps gl in
+  tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
+  
+let default_full_auto gl = full_auto !default_search_depth gl
+(***********************************************************************)
+
+let blast_tactic = ref (free_try default_full_auto)
+;;
+
+let blast_auto = (free_try default_full_auto)
+(*                  (tclTHEN (free_try default_full_auto)
+			  (free_try (my_full_eauto 2)))
+*)
+;;
+let blast_simpl = (free_try (reduce Simpl []))
+;;
+let blast_induction1 = 
+    (free_try (tclTHEN (tclTRY intro)
+		       (tclTRY (tclLAST_HYP simplest_elim))))
+;;
+let blast_induction2 = 
+    (free_try (tclTHEN (tclTRY (tclTHEN intro intro))
+		       (tclTRY (tclLAST_HYP simplest_elim))))
+;;
+let blast_induction3 = 
+    (free_try (tclTHEN (tclTRY (tclTHEN intro (tclTHEN intro intro)))
+		       (tclTRY (tclLAST_HYP simplest_elim))))
+;;
+
+blast_tactic :=
+  (tclORELSE (tclCOMPLETE blast_auto)
+  (tclORELSE (tclCOMPLETE (tclTHEN blast_simpl blast_auto))
+  (tclORELSE (tclCOMPLETE (tclTHEN blast_induction1
+                          (tclTHEN blast_simpl blast_auto)))
+  (tclORELSE (tclCOMPLETE (tclTHEN blast_induction2
+                          (tclTHEN blast_simpl blast_auto)))
+             (tclCOMPLETE (tclTHEN blast_induction3
+                          (tclTHEN blast_simpl blast_auto)))))))
+;;
+(*
+blast_tactic := (tclTHEN (free_try default_full_auto)
+			 (free_try (my_full_eauto 4)))
+;;
+*)
+
+let vire_extvar s =
+   let interro = ref false in
+   let interro_pos = ref 0 in
+   for i=0 to (length s)-1 do
+     if get s i = '?'
+     then (interro := true;
+           interro_pos := i)
+     else if (!interro && 
+              (List.mem (get s i)
+			['0';'1';'2';'3';'4';'5';'6';'7';'8';'9']))
+     then set s i ' '
+     else interro:=false
+   done;
+   s
+;;
+
+let blast gls =
+   let leaf g = {
+      status = Incomplete_proof;
+      subproof = None;
+      goal = g;
+      ref = None } in
+     try (let (sgl,v) as res = !blast_tactic gls in
+	  let {it=lg} = sgl in
+          if lg = [] 
+          then (let pf = v (List.map leaf (sig_it sgl)) in
+                let sign = (sig_it gls).evar_hyps in
+                let x = print_subscript 
+                     (sig_sig gls) sign pf in
+		msgnl (hov 0 (str"Blast ==> " ++ x));
+                let x = print_subscript 
+                     (sig_sig gls) sign pf in
+                let tac_string =
+                pp_string  (hov 0 x ) in
+    (* on remplace les ?1 ?2 ... de refine par ? *)
+		parse_tac ((vire_extvar tac_string)
+			   ^ ".")
+		)
+	  else (msgnl (hov 0 (str"Blast failed to prove the goal..."));
+		failwith "echec de blast"))
+     with _ -> failwith "echec de blast"
+;;
+
+let blast_tac display_function = function 
+          | ((Integer n)::_) as l -> 
+                 (function g ->
+                    let exp_ast = (blast g) in
+                     (display_function (ast_to_ct exp_ast);
+                       tclIDTAC g))
+          |  _ -> failwith "expecting other arguments";;
+
+let blast_tac_txt = 
+  blast_tac (function x -> msgnl(Printer.gentacpr (ct_to_ast x)));;
+
+overwriting_add_tactic "Blast1" blast_tac_txt;;
+
+(*
+Grammar tactic ne_numarg_list : list :=
+  ne_numarg_single [numarg($n)] ->[$n]
+| ne_numarg_cons [numarg($n) ne_numarg_list($ns)] -> [ $n ($LIST $ns) ].
+Grammar tactic simple_tactic : ast :=
+  blast1 [ "Blast1" ne_numarg_list($ns) ] ->
+         [ (Blast1 ($LIST $ns)) ].
+
+
+
+PATH=/usr/local/bin:/usr/bin:$PATH
+COQTOP=d:/Tools/coq-7.0-3mai
+CAMLLIB=/usr/local/lib/ocaml
+CAMLP4LIB=/usr/local/lib/camlp4
+export CAMLLIB
+export COQTOP
+export CAMLP4LIB 
+d:/Tools/coq-7.0-3mai/bin/coqtop.byte.exe 
+Drop.
+#use "/cygdrive/D/Tools/coq-7.0-3mai/dev/base_include";;
+*)
diff --git a/contrib/interface/blast.mli b/contrib/interface/blast.mli
new file mode 100644
index 0000000000..e8bcf95c63
--- /dev/null
+++ b/contrib/interface/blast.mli
@@ -0,0 +1,5 @@
+val blast_tac : (Ctast.t -> 'a) ->
+    Proof_type.tactic_arg list ->
+    Proof_type.goal Tacmach.sigma ->
+    Proof_type.goal list Proof_type.sigma * Proof_type.validation;;
+
diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml
index 00db51adf7..fd60e1e61f 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml
@@ -1,7 +1,7 @@
 
 (*Toplevel loop for the communication between Coq and Centaur *)
 open Names;;
-open Nameops
+open Nameops;;
 open Util;;
 open Ast;;
 open Term;;
@@ -34,6 +34,7 @@ open Ascent;;
 open Translate;;
 open Name_to_ast;;
 open Pbp;;
+open Blast;;
 open Dad;;
 open Debug_tac;;
 open Search;;
@@ -67,7 +68,7 @@ let rec string_of_path p =
               | i::p -> (string_of_int i)^" "^ (string_of_path p)
 ;;
 let print_path p =
-    output_results_nl (str "Path:" ++ str (string_of_path p))
+    output_results_nl (str "Path:" ++ str  (string_of_path p))
 ;;
 
 let kill_proof_node index =
@@ -83,8 +84,8 @@ let kill_proof_node index =
 (*Message functions, the text of these messages is recognized by the protocols *)
 (*of CtCoq                                                                     *)
 let ctf_header message_name request_id =
-  fnl () ++ str "message" ++ fnl () ++ str message_name ++ fnl () ++ 
-  int request_id ++ fnl ();;
+ fnl () ++ str "message" ++ fnl() ++ str message_name ++ fnl() ++
+ int request_id ++ fnl();;
 
 let ctf_acknowledge_command request_id command_count opt_exn =
   let goal_count, goal_index = 
@@ -95,14 +96,14 @@ let ctf_acknowledge_command request_id command_count opt_exn =
         g_count, (min g_count !current_goal_index)
     else
       (0, 0) in
-  (ctf_header "acknowledge" request_id ++
-   int command_count ++ fnl () ++ 
-   int goal_count ++ fnl () ++ 
-   int goal_index ++ fnl () ++ 
-   str !current_proof_name ++ fnl () ++
-   (match opt_exn with
-	Some e -> Errors.explain_exn e
-      | None -> mt ()) ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
+   (ctf_header "acknowledge" request_id ++
+    int command_count ++ fnl() ++
+    int goal_count ++ fnl () ++
+    int goal_index ++ fnl () ++
+    str !current_proof_name ++ fnl() ++
+    (match opt_exn with
+      Some e -> Errors.explain_exn e
+    | None -> mt ()) ++ fnl() ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
 
 let ctf_undoResults = ctf_header "undo_results";;
 
@@ -117,37 +118,36 @@ let ctf_Location = ctf_header "location";;
 let ctf_StateMessage = ctf_header "state";;
 
 let ctf_PathGoalMessage () =
-  fnl () ++ str "message" ++ fnl () ++ str "single_goal" ++ fnl ();;
+ fnl () ++ str "message" ++ fnl () ++ str "single_goal" ++ fnl ();;
 
 let ctf_GoalReqIdMessage = ctf_header "single_goal_state";;
 
 let ctf_NewStateMessage = ctf_header "fresh_state";;
 
-let ctf_SavedMessage () = fnl () ++ str "message" ++ fnl () ++ str "saved" ++ fnl ();;
+let ctf_SavedMessage () = fnl () ++ str "message" ++ fnl () ++
+			  str "saved" ++ fnl();;
 
 let ctf_KilledMessage req_id ngoals =
  ctf_header "killed" req_id ++ int ngoals ++ fnl ();;
 
 let ctf_AbortedAllMessage () =
- fnl () ++ str "message" ++ fnl () ++ str "aborted_all" ++ fnl ();;
+  fnl() ++ str "message" ++ fnl() ++ str "aborted_all" ++ fnl();;
 
 let ctf_AbortedMessage request_id na =
-  fnl () ++ str "message" ++ fnl () ++ str "aborted_proof" ++ fnl () ++ 
-  int request_id ++ fnl () ++
-  str na ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();;
+  ctf_header "aborted_proof" request_id ++ str na ++ fnl () ++ 
+  str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();;
 
 let ctf_UserErrorMessage request_id stream =
-  let stream = guarded_force_eval_stream stream in
-  fnl () ++ str "message" ++ fnl () ++ str "user_error" ++ fnl () ++ 
-  int request_id ++ fnl () ++
-  stream ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();;
+ let stream = guarded_force_eval_stream stream in
+ ctf_header "user_error" request_id ++ stream ++ fnl() ++
+ str "E-n-d---M-e-s-s-a-g-e" ++ fnl();;
 
 let ctf_ResetInitialMessage () =
-  fnl () ++ str "message" ++ fnl () ++ str "reset_initial" ++ fnl ();;
+ fnl () ++ str "message" ++ fnl () ++ str "reset_initial" ++ fnl ();;
 
 let ctf_ResetIdentMessage request_id s =
-  fnl () ++ str "message" ++ fnl () ++ str "reset_ident" ++ fnl () ++ int request_id ++ fnl () ++
-  str s ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();;
+ ctf_header "reset_ident" request_id ++ str s ++ fnl () ++
+  str  "E-n-d---M-e-s-s-a-g-e" ++ fnl();;
 
 type vtp_tree =
   | P_rl of ct_RULE_LIST
@@ -219,7 +219,6 @@ let show_nth n =
   try
     let pf = proof_of_pftreestate (get_pftreestate()) in
     if (!text_proof_flag<>"off") then
-(*      errorlabstrm "debug" [< str "text printing unplugged" >]*)
        (if n=0
 	   then output_results (ctf_TextMessage !global_request_id)
                                (Some (P_text (show_proof !text_proof_flag [])))
@@ -248,9 +247,10 @@ let filter_by_module_from_varg_list (l:vernac_arg list) =
 let add_search (global_reference:global_reference) assumptions cstr =
   try 
     let env = Global.env() in
-    let id_string =
-      string_of_qualid (Nametab.shortest_qualid_of_global env global_reference) in
-    let ast = 
+  let id_string =
+    string_of_qualid (Nametab.shortest_qualid_of_global env 
+			global_reference) in
+  let ast = 
     try
       CT_premise (CT_ident id_string, translate_constr assumptions cstr)
     with Not_found ->
@@ -275,16 +275,13 @@ let print_check (ast, judg) =
       with UserError(f,str) ->
            raise(UserError(f,
 			   Ast.print_ast 
-			     (ast_of_constr true (Global.env()) value) ++
-			   fnl () ++ str))) 
- in
+				(ast_of_constr true (Global.env()) value) ++
+			      fnl () ++ str ))) in
  let type_ct_ast =
      (try translate_constr (Global.env()) typ
       with UserError(f,str) ->
            raise(UserError(f, Ast.print_ast (ast_of_constr true (Global.env())
-					       value) ++
-				 fnl () ++ str))) 
- in
+					       value) ++ fnl() ++ str))) in
  ((ctf_SearchResults !global_request_id),
  (Some  (P_pl
   (CT_premises_list
@@ -309,30 +306,36 @@ and ntyp = nf_betaiota typ in
 
 
 (* The following function is copied from globpr in env/printer.ml *)
-let globcv = function
-  | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) ->
-      let env = Global.env() in
-      convert_qualid
-	 (Nametab.shortest_qualid_of_global env (IndRef(sp,tyi)))
-  | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) ->
-      let env = Global.env() in
-      convert_qualid
-          (Nametab.shortest_qualid_of_global env (ConstructRef ((sp, tyi), i)))
+let globcv x =
+  let env = Global.env() in 
+    match x with
+      | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) ->
+	  let env = Global.env() in
+	    convert_qualid
+	      (Nametab.shortest_qualid_of_global env (IndRef(sp,tyi)))
+      | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) ->
+	  convert_qualid
+            (Nametab.shortest_qualid_of_global env
+	       (ConstructRef ((sp, tyi), i)))
   | _ -> failwith "globcv : unexpected value";;
 
 let pbp_tac_pcoq =
-    pbp_tac (function x -> 
+    pbp_tac (function (x:Ctast.t) -> 
       output_results
-  	(fnl () ++ str "message" ++ fnl () ++ str "pbp_results" ++ fnl () ++
-	 int !global_request_id ++  fnl ())
-	(Some (P_t(xlate_tactic x))));;
+        (ctf_header "pbp_results" !global_request_id)
+       (Some (P_t(xlate_tactic x))));;
+
+let blast_tac_pcoq =
+    blast_tac (function (x:Ctast.t) -> 
+      output_results
+	(ctf_header "pbp_results" !global_request_id)
+       (Some (P_t(xlate_tactic x))));;
 
 
 let dad_tac_pcoq =
   dad_tac(function x -> 
     output_results
-    (fnl () ++ str "message" ++ fnl () ++ str "pbp_results" ++ fnl () ++
-       int !global_request_id ++  fnl ())
+    (ctf_header "pbp_results" !global_request_id)
     (Some (P_t(xlate_tactic x))));;
 
 let search_output_results () =
@@ -351,8 +354,9 @@ let debug_tac2_pcoq = function
 	try
 	  let result = report_error ast the_goal the_ast the_path [] g in
 	  (errorlabstrm "DEBUG TACTIC"
-	    (str "no error here " ++ fnl () ++ pr_goal (sig_it g) ++
-	     fnl () ++ str "the tactic is" ++ fnl ()  ++ Printer.gentacpr ast);
+	     (str "no error here " ++ fnl () ++ pr_goal (sig_it g) ++
+	      fnl () ++ str "the tactic is" ++ fnl () ++
+	      Printer.gentacpr ast);
 	   result)
 	with
 	  e ->
@@ -487,7 +491,7 @@ let command_changes = [
 	      if kind = "LETTOP" && not(refining ()) then
 		errorlabstrm "StartProof"
 		  (str
-                     "Let declarations can only be used in proof editing mode"
+		     "Let declarations can only be used in proof editing mode"
 		  );
 		let str = (string_of_id s) in
 		start_proof_com (Some s) stre c;
@@ -600,12 +604,12 @@ let command_changes = [
    function
        (VARG_QUALID qid)::l ->
          (fun () -> 
-            ctv_SEARCH_LIST:=[];
+           ctv_SEARCH_LIST:=[];
 	    let global_ref = Nametab.global dummy_loc qid in
-            filtered_search
-              (filter_by_module_from_varg_list l)
-	      add_search (Nametab.locate qid);
-	    search_output_results())
+           filtered_search
+             (filter_by_module_from_varg_list l)
+	     add_search (Nametab.locate qid);
+	   search_output_results())
      |	_ -> failwith "bad form of arguments");
 
   ("SearchRewrite",
@@ -697,8 +701,7 @@ let command_changes = [
 	 (fun () -> 
 	   let results = dad_rule_names() in
 	   output_results
-	     (fnl () ++ str "message" ++ fnl () ++ str "dad_rule_names" ++ fnl () ++
-	      int !global_request_id ++ fnl ())
+	     (ctf_header "dad_rule_names" !global_request_id)
 	     (Some (P_ids
 		      (CT_id_list
 			 (List.map (fun s -> CT_ident s) results)))))
@@ -741,6 +744,7 @@ let start_pcoq_mode debug =
     set_xlate_mut_stuff (fun x ->Ctast.ast_to_ct (globcv (Ctast.ct_to_ast x)));
     declare_in_coq();
     add_tactic "PcoqPbp" pbp_tac_pcoq;
+    add_tactic "PcoqBlast" blast_tac_pcoq;
     add_tactic "Dad" dad_tac_pcoq;
     add_tactic "CtDebugTac" debug_tac2_pcoq;
     add_tactic "CtDebugTac2" debug_tac2_pcoq;
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index fad5c1e341..671338002a 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -43,24 +43,29 @@ let print_parse_results n msg =
   flush stdout;;
 
 let ctf_SyntaxErrorMessage reqid pps =
- (fnl () ++ str "message" ++ fnl () ++ str "syntax_error" ++ fnl () ++ int reqid ++ fnl () ++
-   pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
+ fnl () ++ str "message" ++ fnl () ++ str "syntax_error" ++ fnl () ++
+   int reqid ++ fnl () ++
+   pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();;
 let ctf_SyntaxWarningMessage reqid pps =
- (fnl () ++ str "message" ++ fnl () ++ str "syntax_warning" ++ fnl () ++ int reqid ++ fnl () ++
-   pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
+  fnl () ++  str "message" ++ fnl () ++ str "syntax_warning" ++ fnl () ++
+  int reqid ++ fnl () ++ pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl();;
 
 let ctf_FileErrorMessage reqid pps =
- (fnl () ++ str "message" ++ fnl () ++ str "file_error" ++ fnl () ++ int reqid ++ fnl () ++
-   pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
+  fnl () ++ str "message" ++ fnl () ++ str "file_error" ++ fnl () ++
+  int reqid ++ fnl () ++ pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++
+  fnl ();;
 
 (*In the code for CoqV6.2, the require_module call is encapsulated in
   a function "without_mes_ambig".  Here I have supposed that this
   function has no effect on parsing *)
 let try_require_module import specif name fname =
- try Library.require_module (if specif = "UNSPECIFIED" then None
-  else Some (specif = "SPECIFICATION")) (Nametab.make_short_qualid (Names.id_of_string name)) fname (import = "IMPORT")
+ try Library.require_module 
+   (if specif = "UNSPECIFIED" then None
+    else Some (specif = "SPECIFICATION"))
+   (Nametab.make_short_qualid (Names.id_of_string name))
+   fname (import = "IMPORT")
  with
- | e -> msgnl (str "Reinterning of " ++ str name ++ str " failed");;
+   | e -> msgnl (str "Reinterning of " ++ str name ++ str " failed");;
 
 let execute_when_necessary ast =
  (match ast with
@@ -82,20 +87,24 @@ let parse_to_dot =
   let rec dot st = match Stream.next st with
     | ("", ".") -> ()
     | ("EOI", "") -> raise End_of_file
-    | _ -> dot st
-  in 
-  Gram.Entry.of_parser "Coqtoplevel.dot" dot;;
+    | _ -> dot st in
+    Gram.Entry.of_parser "Coqtoplevel.dot" dot;;
 
 let rec discard_to_dot stream =
   try Gram.Entry.parse parse_to_dot (Gram.parsable stream) with
   | Stdpp.Exc_located(_, Token.Error _) -> discard_to_dot stream;;
 
-let rec decompose_string s n =
+let rec decompose_string_aux s n =
     try let index = String.index_from s n '\n' in
             (Ctast.str (String.sub s n (index - n)))::
-            (decompose_string s (index + 1))
+            (decompose_string_aux s (index + 1))
     with Not_found -> [Ctast.str(String.sub s n ((String.length s) - n))];;
 
+let decompose_string s n =
+  match decompose_string_aux s n with
+      (Ctast.Str(_,""))::tl -> tl
+    | a -> a;;
+
 let make_string_list file_chan fst_pos snd_pos =
     let len = (snd_pos - fst_pos) in
     let s = String.create len in
@@ -146,15 +155,17 @@ let parse_command_list reqid stream string_list =
     let rec parse_whole_stream () =
     let this_pos = Stream.count stream in
     let first_ast = 
-        try option_app Ctast.ast_to_ct (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream))
+        try option_app 
+	  Ctast.ast_to_ct (Gram.Entry.parse 
+			       Pcoq.main_entry (Gram.parsable stream))
         with
         | (Stdpp.Exc_located(l, Stream.Error txt)) as e -> 
           begin
              msgnl (ctf_SyntaxWarningMessage reqid (Errors.explain_exn e));
              try
                 discard_to_dot stream;
-                msgnl (str "debug" ++ fnl () ++ int this_pos ++ fnl () ++ int 
-                  (Stream.count stream));
+                msgnl (str "debug" ++ fnl () ++ int this_pos ++ fnl () ++
+		       int (Stream.count stream));
                 Some( Node(l, "PARSING_ERROR",
                         List.map Ctast.str
                         (get_substring_list string_list this_pos
@@ -172,7 +183,13 @@ let parse_command_list reqid stream string_list =
     match first_ast with
     | Some ast ->
         let ast0 = (execute_when_necessary ast) in
-          xlate_vernac ast::parse_whole_stream()
+          (try xlate_vernac ast
+	  with e ->
+	    xlate_vernac 
+              (Node((0,0), "PARSING_ERROR2",
+               List.map Ctast.str
+		 (get_substring_list string_list this_pos
+		    (Stream.count stream)))))::parse_whole_stream()
     | None -> [] in
     match parse_whole_stream () with
     | first_one::tail -> (P_cl (CT_command_list(first_one, tail)))
@@ -239,56 +256,75 @@ let parse_file_action reqid file_name =
      let file_chan_err = open_in file_name in 
      let stream = Stream.of_channel file_chan in
      let stream_err = Stream.of_channel file_chan_err in
-     match let rec parse_whole_file () =
-            let this_pos = Stream.count stream in
-            match 
-              try
-                let this_ast = 
-                     option_app Ctast.ast_to_ct (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream)) in
-                this_ast
-              with
-            | Stdpp.Exc_located(l,Stream.Error txt ) -> 
-                 msgnl (ctf_SyntaxWarningMessage reqid
-                (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++
-                   Errors.explain_exn 
-                      (Stdpp.Exc_located(l,Stream.Error txt))));
-                 let rec discard_to_dot () =
-                 try Gram.Entry.parse parse_to_dot (Gram.parsable stream)
-                 with Stdpp.Exc_located(_,Token.Error _) -> discard_to_dot()
-                 in (try 
-                     discard_to_dot ();
-                        Some( Node(l, "PARSING_ERROR",
-                       (make_string_list file_chan_err this_pos 
-                       (Stream.count stream))))
-                 with End_of_file -> None)
-            | e ->
-                  begin
-                  Gram.Entry.parse parse_to_dot (Gram.parsable stream);
-                  Some( Node((0,0), "PARSING_ERROR2",
-                       (make_string_list file_chan this_pos 
-                       (Stream.count stream))))
-                  end
-
-            with
-            | Some ast -> let ast0=(execute_when_necessary ast) in 
-                 xlate_vernac ast::parse_whole_file ()
-            | None -> [] in
-           parse_whole_file () with
-      | first_one :: tail ->
-       print_parse_results reqid
-          (P_cl (CT_command_list (first_one, tail)))
-      | [] -> raise (UserError ("parse_file_action", (str "empty file.")))
- with
- | Stdpp.Exc_located(l,Match_failure(_,_,_)) ->
- msgnl
-  (ctf_SyntaxErrorMessage reqid
-  (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++
-  Errors.explain_exn (Stdpp.Exc_located(l,Stream.Error "match failure"))))
- | e ->
- msgnl
-  (ctf_SyntaxErrorMessage reqid
-  (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++
-  Errors.explain_exn e));;
+     let rec discard_to_dot () =
+       try Gram.Entry.parse parse_to_dot (Gram.parsable stream)
+       with Stdpp.Exc_located(_,Token.Error _) -> discard_to_dot() in
+       match let rec parse_whole_file () =
+	 let this_pos = Stream.count stream in
+           match 
+             try
+               let this_ast = 
+		 option_app Ctast.ast_to_ct
+		   (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream)) in
+		 this_ast
+             with
+               | Stdpp.Exc_located(l,Stream.Error txt) -> 
+                   msgnl (ctf_SyntaxWarningMessage reqid
+			    (str "Error with file" ++ spc () ++
+			     str file_name ++ fnl () ++
+			     Errors.explain_exn 
+				 (Stdpp.Exc_located(l,Stream.Error txt))));
+		   (try 
+		      begin
+                      	discard_to_dot ();
+                    	Some( Node(l, "PARSING_ERROR",
+				   (make_string_list file_chan_err this_pos 
+			       	      (Stream.count stream))))
+		      end
+                    with End_of_file -> None)
+               | e ->
+                   begin
+                     Gram.Entry.parse parse_to_dot (Gram.parsable stream);
+                     Some(Node((0,0), "PARSING_ERROR2",
+			       (make_string_list file_chan this_pos 
+				  (Stream.count stream))))
+                   end
+		   
+             with
+               | Some ast ->
+		   let ast0=(execute_when_necessary ast) in 
+		   let term =
+                     (try xlate_vernac ast
+		      with e ->
+                    	print_string ("translation error between " ^
+				      (string_of_int this_pos) ^
+				      " " ^
+				      (string_of_int (Stream.count stream)) ^
+				      "\n");
+		    	xlate_vernac 
+			  (Node((0,0), "PARSING_ERROR2",
+			    	(make_string_list file_chan_err this_pos
+				   (Stream.count stream))))) in 
+		     term::parse_whole_file ()
+               | None -> [] in
+         parse_whole_file () with
+	   | first_one :: tail ->
+	       print_parse_results reqid
+		 (P_cl (CT_command_list (first_one, tail)))
+	   | [] -> raise (UserError ("parse_file_action", str "empty file."))
+       with
+	 | Stdpp.Exc_located(l,Match_failure(_,_,_)) ->
+	     msgnl
+	       (ctf_SyntaxErrorMessage reqid
+		  (str "Error with file" ++ spc () ++ str file_name ++ 
+		   fnl () ++
+		     Errors.explain_exn
+		       (Stdpp.Exc_located(l,Stream.Error "match failure"))))
+	 | e ->
+	     msgnl
+	       (ctf_SyntaxErrorMessage reqid
+		  (str "Error with file" ++ spc () ++ str file_name ++
+		   fnl () ++ Errors.explain_exn e));;
 
 (* This function is taken from Mltop.add_path *)
 
@@ -302,7 +338,7 @@ let add_path dir coq_dirpath =
 
 let convert_string d =
   try Names.id_of_string d
-  with _ -> failwith "caught"
+  with _ -> failwith ("could not convert " ^ d)
 
 let add_rec_path dir coq_dirpath =
   let dirs = all_subdirs dir in
@@ -345,11 +381,12 @@ let load_syntax_action reqid module_name =
  msgnl (mt ());
  msgnl
   (fnl () ++ str "error while loading syntax module " ++ str module_name ++
-  str ": " ++ str label ++ fnl () ++ pp_stream)
+   str ": " ++ str label ++ fnl () ++ pp_stream)
  | e ->
   msgnl (mt ());
   msgnl
-   (fnl () ++ str "message" ++ fnl () ++ str "load_error" ++ fnl () ++ int reqid ++ fnl ());
+   (fnl () ++ str "message" ++ fnl () ++ str "load_error" ++ fnl () ++
+    int reqid ++ fnl ());
   ();;
 
 let coqparser_loop inchan =
@@ -373,25 +410,14 @@ Libobject.relax true;
        else
 	 (msgnl (str "could not find the value of COQDIR"); exit 1) in
      begin
-       add_rec_path (Filename.concat coqdir "theories") (Names.make_dirpath [Nameops.coq_root]);
-       add_path (Filename.concat coqdir "tactics") (Names.make_dirpath [Nameops.coq_root]);
-       add_rec_path (Filename.concat coqdir "contrib") (Names.make_dirpath [Nameops.coq_root]);
+       add_rec_path (Filename.concat coqdir "theories")
+	 (Names.make_dirpath [Nameops.coq_root]);
+       add_path (Filename.concat coqdir "tactics")
+	 	 (Names.make_dirpath [Nameops.coq_root]);
+       add_rec_path (Filename.concat coqdir "contrib")
+	 (Names.make_dirpath [Nameops.coq_root]);
        List.iter (fun a -> msgnl (str a)) (get_load_path())
      end;
-(try 
-  (match create_entry (get_univ "nat") "number" ETast with
-     (Ast number) ->
-      Gram.extend number None
-	[None, None, 
-	 [[Gramext.Stoken ("INT", "")],
-	 Gramext.action 
-	    (fun s loc ->
-		 Node((0,0),"XTRA",[Str((0,0),"omega_integer_for_ctcoq");
-				 Num((0,0),int_of_string s)]))]]
-   | _ -> msgnl (str "unpredicted behavior of Grammar.extend"))
-
- with
-   e -> msgnl (str "could not add a parser for numbers"));
 (let vernacrc =
    try
      Sys.getenv "VERNACRC"
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 13e307a47c..2e92dd7c9d 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -1,6 +1,4 @@
 (* A proof by pointing algorithm. *)
-
-
 open Util;;
 open Names;;
 open Term;;
@@ -20,14 +18,21 @@ open Typing;;
 open Pp;;
 
 (* get_hyp_by_name : goal sigma -> string -> constr,
-   looks up for an hypothesis, from its name *)
+   looks up for an hypothesis (or a global constant), from its name *)
 let get_hyp_by_name g name =
   let evd = project g in
   let env = pf_env g in
-  let judgment = 
-    Pretyping.understand_judgment 
-      evd env (RVar(dummy_loc, id_of_string name)) in
-    judgment.uj_type;;
+  try (let judgment = 
+         Pretyping.understand_judgment 
+          evd env (RVar(dummy_loc, id_of_string name)) in
+       ("hyp",judgment.uj_type))
+(* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up...
+   Loïc *)
+  with _ -> (let parse_ast = Pcoq.parse_string Pcoq.Constr.constr in
+             let parse s = Astterm.interp_constr Evd.empty (Global.env())
+	          (parse_ast s) in
+             ("cste",type_of (Global.env()) Evd.empty (parse name)))
+;;
 
 type pbp_rule = (identifier list *
                     string list *
@@ -62,8 +67,9 @@ let get_name_from_intro = function
 let make_clears =  function
     [] -> Node(zz, "Idtac",[])
   | str_list ->
-      Node(zz,"Clear",
-	   [Node(zz, "CLAUSE", List.map (function s -> Nvar(zz,s)) str_list)]);;
+      Node(zz, "TRY", [Node(zz,"Clear",
+	   [Node(zz, "CLAUSE", List.map (function s -> Nvar(zz,s)) str_list)])
+	       ]);;
 
 let add_clear_names_if_necessary tactic clear_names =
     match clear_names with
@@ -176,7 +182,7 @@ let (imply_elim2: pbp_rule) = function
   | _ -> None;;
 
 let reference dir s =
-  let dir = make_dirpath 
+  let dir = make_dirpath
               (List.map id_of_string (List.rev ("Coq"::"Init"::[dir]))) in
   let id = id_of_string s in
   try 
@@ -185,9 +191,7 @@ let reference dir s =
     anomaly ("Coqlib: cannot find "^
 	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))
 
-let constant dir s =
-  Declare.constr_of_reference (reference dir s);;
-
+let constant dir s =  Declare.constr_of_reference (reference dir s);;
 
 let andconstr: unit -> constr = Coqlib.build_coq_and;;
 let prodconstr () = constant "Datatypes" "prod";;
@@ -544,6 +548,9 @@ let default_ast optname constr path =
                    [Node(zz, "Exact",[Node(zz,"COMMAND",[Nvar(zz,a)])])]);;
 
 (* This is the main proof by pointing function. *)
+(* avoid: les noms a ne pas utiliser *)
+(* final_cmd: la fonction appelee par defaut *)
+(* opt_name: eventuellement le nom de l'hypothese sur laquelle on agit *)
 
 let rec pbpt final_cmd avoid clear_names clear_flag opt_name constr path =
   let rec try_all_rules rl =
@@ -645,7 +652,7 @@ let cleanup_clears empty_allowed names str_list other =
 		[]
 	      else [Node(zz,"Idtac",[])]
           | _ -> other)
-  | l -> Node(zz, "Clear", [Node(zz,"CLAUSE", l)])::other;;
+  | l -> Node(zz, "TRY", [Node(zz, "Clear", [Node(zz,"CLAUSE", l)])])::other;;
 
 
 (* This function takes care of compacting instanciations of universal
@@ -661,7 +668,7 @@ let rec optim3 str_list = function
 	     | Some s -> optim3_aux true (s::str_list)
                             (Node(a, "Generalize",
                                 [merge_ast_in_command com1 com2])::others))
-	|( Node(a,"Clear", [Node(_,"CLAUSE", names)]))::other ->
+	|( Node(zz, "TRY", [Node(a,"Clear", [Node(_,"CLAUSE", names)])]))::other ->
 	    cleanup_clears empty_allowed names str_list other
 	| [Node(a,"TACLIST",branches)] ->
 	    [Node(a,"TACLIST",List.map (optim3 str_list) branches)]
@@ -686,9 +693,16 @@ let pbp_tac display_function = function
             (Identifier a)::l -> 
                  (function g ->
                     let str = (string_of_id a) in
+		    let (ou,tstr) = (get_hyp_by_name g str) in
 		    let exp_ast =
-		      pbpt default_ast  (pf_ids_of_hyps g)
-                        [] false (Some str) (kind_of_term (get_hyp_by_name g str))
+		      pbpt default_ast
+		        (match ou with
+			       "hyp" ->(pf_ids_of_hyps g)
+			       |_ -> (a::(pf_ids_of_hyps g)))
+                        []
+			false
+			(Some str)
+			(kind_of_term tstr)
                         (tactic_args_to_ints l) in
                     (display_function (optim exp_ast);
                         tclIDTAC g))
@@ -704,3 +718,5 @@ let pbp_tac display_function = function
                      (display_function (default_ast None (pf_concl g) []);
                       tclIDTAC g))
           |  _ -> failwith "expecting other arguments";;
+
+
diff --git a/contrib/interface/vernacrc b/contrib/interface/vernacrc
index 092bc07090..b66f1e4c11 100644
--- a/contrib/interface/vernacrc
+++ b/contrib/interface/vernacrc
@@ -10,6 +10,7 @@ load_syntax_file 21 Equality
 load_syntax_file 22 Inv
 load_syntax_file 26 Tauto
 load_syntax_file 34 Omega
+load_syntax_file 27 Ring
 quiet_parse_string
 Goal a.
 && END--OF--DATA
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 7782203229..597553cd52 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -457,7 +457,9 @@ and fCONTEXT_RULE = function
 and fCONVERSION_FLAG = function
 | CT_beta -> fNODE "beta" 0
 | CT_delta -> fNODE "delta" 0
+| CT_evar -> fNODE "evar" 0
 | CT_iota -> fNODE "iota" 0
+| CT_zeta -> fNODE "zeta" 0
 and fCONVERSION_FLAG_LIST = function
 | CT_conversion_flag_list l ->
    (List.iter fCONVERSION_FLAG l);
@@ -479,8 +481,8 @@ and fCO_IND = function
 | CT_coerce_DEFN_to_DEFN_OR_THM x -> fDEFN x
 | CT_coerce_THM_to_DEFN_OR_THM x -> fTHM x
 and fDEF_BODY = function
+| CT_coerce_CONTEXT_PATTERN_to_DEF_BODY x -> fCONTEXT_PATTERN x
 | CT_coerce_EVAL_CMD_to_DEF_BODY x -> fEVAL_CMD x
-| CT_coerce_FORMULA_to_DEF_BODY x -> fFORMULA x
 and fDEP = function
 | CT_dep x -> fATOM "dep";
    (f_atom_string x);
@@ -590,9 +592,6 @@ and fFORMULA = function
    fFORMULA x2;
    fFORMULA x3;
    fNODE "letin" 3
-| CT_metac(x1) ->
-   fINT x1;
-   fNODE "metac" 1
 | CT_prodc(x1, x2) ->
    fBINDER x1;
    fFORMULA x2;
@@ -632,7 +631,10 @@ and fHINT_EXPRESSION = function
 and fID = function
 | CT_ident x -> fATOM "ident";
    (f_atom_string x);
-   print_string "\n"and fIDENTITY_OPT = function
+   print_string "\n"| CT_metac(x1) ->
+   fINT x1;
+   fNODE "metac" 1
+and fIDENTITY_OPT = function
 | CT_coerce_NONE_to_IDENTITY_OPT x -> fNONE x
 | CT_identity -> fNODE "identity" 0
 and fID_LIST = function
@@ -728,6 +730,19 @@ and fIN_OR_OUT_MODULES = function
 | CT_out_modules(x1) ->
    fID_NE_LIST x1;
    fNODE "out_modules" 1
+and fLET_CLAUSE = function
+| CT_let_clause(x1, x2) ->
+   fID x1;
+   fLET_VALUE x2;
+   fNODE "let_clause" 2
+and fLET_CLAUSES = function
+| CT_let_clauses(x,l) ->
+   fLET_CLAUSE x;
+   (List.iter fLET_CLAUSE l);
+   fNODE "let_clauses" (1 + (List.length l))
+and fLET_VALUE = function
+| CT_coerce_DEF_BODY_to_LET_VALUE x -> fDEF_BODY x
+| CT_coerce_TACTIC_COM_to_LET_VALUE x -> fTACTIC_COM x
 and fLOCAL_OPT = function
 | CT_coerce_NONE_to_LOCAL_OPT x -> fNONE x
 | CT_local -> fNODE "local" 0
@@ -749,6 +764,16 @@ and fMATCH_PATTERN_NE_LIST = function
    fMATCH_PATTERN x;
    (List.iter fMATCH_PATTERN l);
    fNODE "match_pattern_ne_list" (1 + (List.length l))
+and fMATCH_TAC_RULE = function
+| CT_match_tac_rule(x1, x2) ->
+   fCONTEXT_PATTERN x1;
+   fLET_VALUE x2;
+   fNODE "match_tac_rule" 2
+and fMATCH_TAC_RULES = function
+| CT_match_tac_rules(x,l) ->
+   fMATCH_TAC_RULE x;
+   (List.iter fMATCH_TAC_RULE l);
+   fNODE "match_tac_rules" (1 + (List.length l))
 and fNATURAL_FEATURE = function
 | CT_contractible -> fNODE "contractible" 0
 | CT_implicit -> fNODE "implicit" 0
@@ -1088,15 +1113,18 @@ and fTACTIC_COM = function
 | CT_left(x1) ->
    fSPEC_LIST x1;
    fNODE "left" 1
-| CT_lettac(x1, x2, x3) ->
-   fID x1;
-   fFORMULA x2;
-   fUNFOLD_NE_LIST x3;
-   fNODE "lettac" 3
+| CT_lettac(x1, x2) ->
+   fLET_CLAUSES x1;
+   fLET_VALUE x2;
+   fNODE "lettac" 2
 | CT_match_context(x,l) ->
    fCONTEXT_RULE x;
    (List.iter fCONTEXT_RULE l);
    fNODE "match_context" (1 + (List.length l))
+| CT_match_tac(x1, x2) ->
+   fLET_VALUE x1;
+   fMATCH_TAC_RULES x2;
+   fNODE "match_tac" 2
 | CT_move_after(x1, x2) ->
    fID x1;
    fID x2;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index c7552847f3..7f38ca0d27 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -42,16 +42,12 @@ Hashtbl.add type_table "Coq.Init.Datatypes.prod"
 Hashtbl.add type_table "Coq.Init.Datatypes.nat"
   [|[|"";"O"; "S"|]|];;
 
-(* //menage a faire....*)
-Hashtbl.add type_table "Coq.Zarith.fast_integer.Z"
-[|[|"";"ZERO";"POS";"NEG"|]|];;
 Hashtbl.add type_table "Coq.ZArith.fast_integer.Z"
 [|[|"";"ZERO";"POS";"NEG"|]|];;
-(*//itou *)
-Hashtbl.add type_table "Coq.Zarith.fast_integer.positive"
-[|[|"";"xI";"xO";"XH"|]|];;
+
+
 Hashtbl.add type_table "Coq.ZArith.fast_integer.positive"
-[|[|"";"xI";"xO";"XH"|]|];;
+[|[|"";"xI";"xO";"xH"|]|];;
 
 (*The following two codes are added to cope with the distinction
   between ocaml and caml-light syntax while using ctcaml to
@@ -71,7 +67,7 @@ let string_of_node_loc the_node =
   match loc the_node with
       (a,b) -> "(" ^ (string_of_int a) ^ ", " ^ (string_of_int b) ^ ")";;
 
-let xlate_error s = error ("Translation error: " ^ s);;
+let xlate_error s = failwith ("Translation error: " ^ s);;
 
 type astrecurse =   Rbinder of ct_ID_OPT * astrecurse
                   | Rform of ct_FORMULA
@@ -98,6 +94,10 @@ let ctv_ID_OPT_OR_ALL_ALL = CT_all;;
 
 let ctv_SPEC_OPT_NONE = CT_coerce_NONE_to_SPEC_OPT CT_none;;
 
+let ct_coerce_FORMULA_to_DEF_BODY x =
+    CT_coerce_CONTEXT_PATTERN_to_DEF_BODY
+    (CT_coerce_FORMULA_to_CONTEXT_PATTERN x);;
+
 let castc x = CT_coerce_TYPED_FORMULA_to_FORMULA x;;
 
 let varc x = CT_coerce_ID_to_FORMULA x;;
@@ -310,6 +310,7 @@ let qualid_to_ct_ID =
 	    | (Nvar(_,s))::l ->  s ^ "." ^ (f l)
 	    | _ -> assert false in
 	  Some(CT_ident (f l))
+    | Node(_, "QUALIDMETA",[Num(_,n)]) -> Some(CT_metac (CT_int n))
     | _ -> None;;
 
 
@@ -322,7 +323,7 @@ let xlate_op the_node opn a b =
  match opn with
  | "META" ->
   (match a, b with
-  | ((Num (_, n)) :: []), [] -> CT_metac (CT_int n)
+  | ((Num (_, n)) :: []), [] -> CT_coerce_ID_to_FORMULA(CT_metac (CT_int n))
   | _, _ -> xlate_error "xlate_op : META ")
  | "ISEVAR" -> CT_existvarc
  | "FORCEIF" ->
@@ -403,15 +404,15 @@ let xlate_op the_node opn a b =
 	      CT_ident(Names.string_of_id
 			 (Nameops.basename (section_path sl))))
   	| _, _ -> xlate_error "xlate_op : MUTIND")
- | "MUTCASE" 
- | "CASE" ->
-     let compute_flag s = 
-       match s with "REC" -> "Match" | "NOREC" -> "Case" | _ -> assert false in
-     (match a, b with
-  	| [Str(_,v)], tl -> make_casec (compute_flag v) tl
-	| [Str(_,v); Str(_,"SYNTH")], tl ->
-	    make_casec (compute_flag v) (Rform CT_existvarc::tl)
-  	| _, _ -> xlate_error "xlate_op : MUTCASE")
+ | "CASE"
+ | "MATCH" ->
+     (let compute_flag s = 
+       	match s with "CASE" -> "Case" | "MATCH" -> "Match" | _ -> assert false in
+	match a, b with
+          | [], tl -> make_casec (compute_flag opn) tl
+      	  | [Str(_, "SYNTH")], tl ->
+              make_casec (compute_flag opn) (Rform CT_existvarc::tl)
+	| _, _ -> assert false)
  | (** string_of_path needs to be investigated.
       *)
    "MUTCONSTRUCT" ->
@@ -465,7 +466,8 @@ let id_to_pattern_var ctid =
      CT_coerce_ID_OPT_to_MATCH_PATTERN (CT_coerce_NONE_to_ID_OPT CT_none)
  | CT_ident id_string ->
      CT_coerce_ID_OPT_to_MATCH_PATTERN 
-       (CT_coerce_ID_to_ID_OPT (CT_ident id_string));;
+       (CT_coerce_ID_to_ID_OPT (CT_ident id_string))
+ | _ -> assert false;;
 
 let rec xlate_cases_pattern cont_function =
  function
@@ -491,6 +493,13 @@ let rec xlate_cases_pattern cont_function =
 	   | CT_coerce_ID_to_FORMULA id -> id_to_pattern_var id
 	   | _ -> assert false)
     | Node(_, s, _) -> xlate_error ("error for a pattern " ^ s)
+    | Path(_,sl) -> 
+        id_to_pattern_var (CT_ident (List.fold_right
+				       (fun a b ->
+					  if b = "" then
+					    a
+					  else
+					    a ^ "." ^ b) sl ""))
     | _ -> xlate_error "Unexpected data while translating a pattern";;
 
 (*This function recognizes and translates let constructs
@@ -504,82 +513,6 @@ let special_case_let_construct cont_function =
 		strip_Rform (cont_function body))))
     | _ -> None;;
 
-(*This function recognizes and translates the integers introduced by P.Cregut.
-  However, it relies on the patterns given in our our version of integer_gram *)
-let compile_decomposed_number cont_function ast =
- (*cdn_rec returns a list of strings that represent the bits in a
-   binary representation of the number. 1 is represented by "xI" and 0 by "xO" *)
- let rec cdn_rec =
-  function
-     | Node (_, "APPLIST", ((Nvar (_, s)) :: args)) as t ->
-      (match s with
-      | "xI" | "xO" ->
-       (match args with
-       | arg :: [] ->
-        let digit_list, head = cdn_rec arg in
-        s::digit_list, head
-       | _ -> xlate_error "bad number of arguments for xI or XO")
-      | it -> [], Some t)
-     | Nvar (_, s) as t ->
-      (match s with
-      | "xH" -> ["xI"], None
-      | _ -> [], Some t)
-     | t -> [], Some t in
- (*when the number will appear as a binary number, we fake it by using base
-   10 when reconstructing the number  (A binary number looks like a decimal number
-   written only with ones and zeros).  Otherwise, we use base 2, respecting
-   the true meaning of each bit. *)
- let rec convert_to_number base =
-  function
-     | [] -> 0
-     | "xI" :: tail -> 1 + base * convert_to_number base tail
-     | "xO" :: tail -> base * convert_to_number base tail
-     | _ -> xlate_error "compile_decomposed_number" in
- match cdn_rec ast with
-  | (*binary representation is only used when constructing an incomplete number *)
-    digit_list, (Some formula) ->
-   CT_incomplete_binary
-    (strip_Rform (cont_function formula),
-    CT_binary (convert_to_number 10 digit_list))
-  | digit_list, None ->
-   CT_int_encapsulator (CT_int (convert_to_number 2 digit_list));;
-
-let special_case_omega_integer cont_function =
- function
-    | Node (_, "XTRA",
-              ((Str (_, "omega_integer_for_ctcoq")) :: ((Num (_, n)) :: []))) ->
-     Some (Rform (CT_int_encapsulator (CT_int n)))
-    | Node (_, "XTRA",
-              ((Str (_, "omega_binary_for_ctcoq")) :: ((Num (_, n)) :: []))) ->
-     Some (Rform (CT_coerce_BINARY_to_FORMULA (CT_binary n)))
-    | Node (_, "XTRA",
-              ((Str (_, "omega_variable_binary_for_ctcoq")) ::
-                (formula :: ((Num (_, n)) :: [])))) ->
-     Some
-      (Rform
-      (CT_incomplete_binary (strip_Rform (cont_function formula), CT_binary n)))
-    | Node (_, "APPLIST",
-              ((Nvar (_, pos_or_neg_string)) ::
-                ((Node (_, "APPLIST", ((Nvar (_, id)) :: (_ :: []))) as number)
-                  :: []))) ->
-     (match pos_or_neg_string with
-     | "POS" ->
-      (match id with
-      | "xI" | "xO" | "xH" ->
-       Some (Rform (compile_decomposed_number cont_function number))
-      | _ -> None)
-     | "NEG" ->
-      (match id with
-      | "xI" | "xO" | "xH" ->
-       Some
-        (Rform
-        (CT_appc
-        (CT_coerce_ID_to_FORMULA (CT_ident "NEG"),
-        CT_formula_ne_list (compile_decomposed_number cont_function number, []))))
-      | _ -> None)
-     | _ -> None)
-    | _ -> None;;
-
 let cvt_binder cont_function =
  function 
     | Node (_,"BINDER", (c :: idl)) ->
@@ -796,7 +729,6 @@ let special_case_S cont_function ast =
 let xlate_formula_special_cases =
  [special_case_qualid;
  special_case_let_construct;
- special_case_omega_integer;
  special_case_fix;
  special_case_cofix;
  special_case_cases;
@@ -920,18 +852,23 @@ let strip_targ_intropatt =
 let rec get_flag_rec =
  function
     | n1 :: tail ->
+     	let conv_id_fun = (fun x -> match qualid_to_ct_ID x with
+                             Some y -> y
+                             | None -> assert false) in
      let conv_flags, red_ids = get_flag_rec tail in
      (match n1 with
       | Node (_, "Beta", []) -> CT_beta::conv_flags, red_ids
       | Node (_, "Delta", []) -> CT_delta::conv_flags, red_ids
       | Node (_, "Iota", []) -> CT_iota::conv_flags, red_ids
+      | Node (_, "Zeta", []) -> CT_zeta::conv_flags, red_ids
+      | Node (_, "Evar", []) -> CT_evar::conv_flags, red_ids
       | Node (_, "Unf", l) ->
        (match red_ids with
-       | CT_unf [] -> conv_flags, CT_unf (List.map xlate_id l)
+       | CT_unf [] -> conv_flags, CT_unf (List.map conv_id_fun l)
        | _ -> error "Cannot specify identifiers to unfold twice")
       | Node (_, "UnfBut", l) ->
        (match red_ids with
-       | CT_unf [] -> conv_flags, CT_unfbut (List.map xlate_id l)
+       | CT_unf [] -> conv_flags, CT_unfbut (List.map conv_id_fun l)
        | _ -> error "Cannot specify identifiers to unfold twice")
       | Node (_, a, _) -> error ("get_flag_rec : unexpected flag " ^ a)
       | _ -> error "get_flag_rec : unexpected flag")
@@ -974,6 +911,8 @@ let tactic_special_case cont_function cvt_arg = function
 let xlate_context_pattern = function
     Node(_,"TERM", [Node(_, "COMMAND", [v])]) -> 
       CT_coerce_FORMULA_to_CONTEXT_PATTERN (xlate_formula v)
+  | Node(_,"SUBTERM", [Node(_,"COMMAND",[v])]) ->
+      CT_context(ctv_ID_OPT_NONE, xlate_formula v)
   | Node(_,"SUBTERM", [Nvar(_, s); Node(_, "COMMAND", [v])]) ->
       CT_context(ctf_ID_OPT_SOME (CT_ident s), xlate_formula v)
   | _ -> assert false;;
@@ -1028,17 +967,29 @@ let rec cvt_arg =
     | Node (_, "COFIXEXP",
               ((Nvar (_, id)) :: ((Node (_, "COMMAND", (c :: []))) :: []))) ->
      Targ_cofixtac (CT_cofixtac (CT_ident id, xlate_formula c))
-    | Node (_, "CLAUSE", l) -> Targ_id_list (CT_id_list (List.map (function
-                                   | Nvar (_, x) -> CT_ident x
-                                   | _ ->
-                                    xlate_error
-                                     "expected identifiers in a CLAUSE") l))
+    | Node ((l1,l2), "CLAUSE", l) ->
+ 	Targ_id_list (CT_id_list 
+			(List.map 
+			   (function
+			      | Node(_, "INHYP", [Nvar (_, x)]) -> CT_ident x
+			      | Node(_, "INHYP", 
+				     [Node(_, "COMMAND",
+					     [Node(_, "META",
+						   [Num (_, x)])])]) ->
+				  CT_metac (CT_int x)
+                              | _ ->
+                                  xlate_error
+                                    ("expected identifiers in a CLAUSE " ^
+				     (string_of_int l1) ^ " " ^
+				    (string_of_int l2))) l))
     | Node (_, "REDEXP", (tac :: [])) -> Targ_redexp (xlate_red_tactic tac)
     | Node (_, "INTROPATTERN", 
           [Node(_,"LISTPATTERN", l)]) -> 
               Targ_intropatt (CT_intro_patt_list(List.map xlate_intro_pattern l))
     | Node(_, "Str", [x]) -> cvt_arg x
-    | Node (_, a, _) -> failwith ("cvt_arg on node " ^ a)
+    | Node ((l1,l2), a, _) -> failwith ("cvt_arg on node " ^ a ^ " at " ^
+				       (string_of_int l1) ^ " " ^
+				       (string_of_int l2))
     | _ -> failwith "cvt_arg"
 and xlate_red_tactic =
  function
@@ -1049,13 +1000,15 @@ and xlate_red_tactic =
      | "Simpl" -> CT_simpl
      | "Fold" -> CT_fold(CT_formula_list[])
      | _ -> xlate_error ("xlate_red_tactic, unexpected singleton " ^ s))
-    | Node (_, "Unfold", unf_list) ->
+    | Node ((l1,l2), "Unfold", unf_list) ->
      let ct_unf_list = List.map (function
          | Node (_, "UNFOLD", qid::nums) ->
 	     (match qualid_to_ct_ID qid with
 		 Some x -> 
 		   CT_unfold_occ (CT_int_list (List.map xlate_int nums), x)
-	       	| _ -> assert false)
+	       	| _ -> failwith ("bad form in Unfold at characters " ^
+                                 (string_of_int l1) ^ " " ^
+				 (string_of_int l2))  )
          | n -> 
 	     xlate_error ("xlate_red_tactic, expected unfold occurrence at " ^
 			  (string_of_node_loc n)))
@@ -1128,19 +1081,66 @@ and xlate_tactic =
      | ((s, l) as it) when (is_tactic_special_case s) ->
 	 tactic_special_case xlate_tactic cvt_arg it
      | "APP", (Nvar(_,s))::l ->
-         let f = fun x -> CT_coerce_FORMULA_to_TACTIC_ARG x in
          let args = 
 	   List.map (function 
-                        Node(_, "COMMAND", [x]) -> f (xlate_formula x)
-		       | x -> f (xlate_formula x)) l in
+                       | Node(_, "COMMAND", [x]) -> 
+			   CT_coerce_FORMULA_to_TACTIC_ARG (xlate_formula x)
+		       | x -> 
+			   CT_coerce_TACTIC_COM_to_TACTIC_ARG(xlate_tactic x))
+	     l in
          let fst,args2 = 
 	   match args with
 	       fst::args2 -> fst, args2
 	     | _ -> assert false in
 	 CT_simple_user_tac(CT_ident s, CT_tactic_arg_list(fst, args2))
+     | "MATCH", exp::rules ->
+        CT_match_tac(mk_let_value exp,
+		     match List.map 
+		       (function 
+			  | Node(_,"MATCHRULE", 
+				 [Node(_,"TERM", [Node(_,"COMMAND", [p])]);
+				 tac]) ->
+			      CT_match_tac_rule(
+			      	CT_coerce_FORMULA_to_CONTEXT_PATTERN 
+						  (xlate_formula p),
+						  mk_let_value tac)
+                          | Node(_,"MATCHRULE", [tac]) ->
+			      CT_match_tac_rule
+				(CT_coerce_FORMULA_to_CONTEXT_PATTERN
+				   CT_existvarc, 
+				   mk_let_value tac)
+			  | Node((l1,l2),s,_) ->
+                             failwith ("problem with match_tac at " ^
+				      (string_of_int l1) ^
+				      " " ^
+				      (string_of_int l2) ^
+				      ": " ^ s)
+			  | _ -> assert false) rules with
+			 | [] -> assert false
+			 | fst::others ->
+			     CT_match_tac_rules(fst, others))
      | "MATCHCONTEXT", rule1::rules ->
 	 CT_match_context(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
+     | "LET", [Node(_, "LETDECL",l);
+               t] -> 
+	 let cvt_clause =
+	   function
+	     | Node(_, "LETCLAUSE", [Nvar(_, s);Node(_,"COMMAND",[v])]) ->
+		 CT_let_clause(CT_ident s,
+			       CT_coerce_DEF_BODY_to_LET_VALUE
+                               (formula_to_def_body v)) 
+	     | Node(_, "LETCLAUSE", [Nvar(_, s); v]) ->
+		 CT_let_clause(CT_ident s,
+			       CT_coerce_TACTIC_COM_to_LET_VALUE
+                               (xlate_tactic v)) 
+	     | Node(_, s, _) -> failwith ("cvt_clause : unexpected " ^ s)
+	     | _ -> assert false in
+	 let cl_l = List.map cvt_clause l in
+         (match cl_l with
+	    | [] -> assert false 
+	    | fst::others ->
+	   	CT_lettac (CT_let_clauses(fst, others), mk_let_value t))
      | s, l -> xlate_tac (s, List.map cvt_arg l))
     | Nvar(_, s) -> ident_tac s
     | the_node -> xlate_error ("xlate_tactic at " ^
@@ -1349,7 +1349,7 @@ and xlate_tac =
        CT_clear (CT_id_ne_list (id, idl))
       | _ -> xlate_error "Clear expects a non empty list of identifiers")
     | (*For translating tactics/Inv.v *)
-      "Inv", [Targ_ident (CT_ident s); Targ_ident id] ->
+      "Inv", [Targ_string (CT_string s); Targ_ident id] ->
      CT_inversion (compute_INV_TYPE_from_string s, id, CT_id_list [])
     | "InvIn", ((Targ_ident (CT_ident s))::((Targ_ident id) :: idlist)) ->
      CT_inversion
@@ -1383,7 +1383,31 @@ and (xlate_context_rule: Ctast.t -> ct_CONTEXT_RULE) =
 	  | _ -> assert false in
 	let hyps, cpat, tactic = xlate_ctxt_rule_aux parts in
 	  CT_context_rule(CT_context_hyp_list hyps, cpat, tactic)
-    | _ -> assert false;;
+    | _ -> assert false
+and (formula_to_def_body : Ctast.t -> ct_DEF_BODY) =
+  function
+    | Node(_, "EVAL", [f;Node(_, "REDEXP", [tac])]) ->
+	(try 
+        CT_coerce_EVAL_CMD_to_DEF_BODY(
+	CT_eval(CT_coerce_NONE_to_INT_OPT CT_none,
+                xlate_red_tactic tac,
+		xlate_formula f))
+	with Failure s ->
+	  failwith ("error raised inside formula_to_def_body " ^
+		    s))
+    | f -> (try ct_coerce_FORMULA_to_DEF_BODY(xlate_formula f)
+            with Failure s -> 
+	      match f with
+		  Node(_,s1, _) ->
+		    failwith ("error raised inside formula_to_def_body (2) " ^
+			      s1 ^ " " ^ s)
+		| _ ->
+		    failwith("error raised inside formula_to_def_body (3) " ^
+			     s))
+and mk_let_value = function 
+    Node(_, "COMMAND", [v]) -> 
+      CT_coerce_DEF_BODY_to_LET_VALUE(formula_to_def_body v)
+  | v -> CT_coerce_TACTIC_COM_to_LET_VALUE(xlate_tactic v);;
 
 let strip_varg_int =
  function
@@ -1532,7 +1556,7 @@ let get_require_flags impexp spec =
 
 let cvt_optional_eval_for_definition c1 optional_eval =
   match optional_eval with
-    None -> CT_coerce_FORMULA_to_DEF_BODY c1
+    None -> ct_coerce_FORMULA_to_DEF_BODY c1
   | Some (Targ_redexp red_com) ->
       CT_coerce_EVAL_CMD_to_DEF_BODY(
       CT_eval(CT_coerce_NONE_to_INT_OPT CT_none,