premier debugage

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

4 files changed, 9 insertions, 17 deletions

diff --git a/tactics/auto.mli b/tactics/auto.mli
index 01a2d5f6dd..333aca1344 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -17,9 +17,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 *)
-  (***TODO
-  | Extern     of CoqAst.t               (* Hint Extern *)
-  ***)
+  | Extern     of Coqast.t               (* Hint Extern *)
 
 type pri_auto_tactic = { 
   hname : identifier;     (* name of the hint *)
@@ -87,10 +85,8 @@ val make_resolve_hyp : identifier -> constr -> (constr * pri_auto_tactic) list
 
 (* [make_extern name pri pattern tactic_ast] *)
 
-(***TODO
 val make_extern :
-  identifier -> int -> constr -> CoqAst.t -> constr * pri_auto_tactic
-***)
+  identifier -> int -> constr -> Coqast.t -> constr * pri_auto_tactic
 
 (* Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints *)
diff --git a/tactics/pattern.ml b/tactics/pattern.ml
index 52b6586b5c..5ff9a6294e 100644
--- a/tactics/pattern.ml
+++ b/tactics/pattern.ml
@@ -28,12 +28,9 @@ let rec whd_replmeta = function
   | DOP2(Cast,c,_) -> whd_replmeta c
   | c -> c
 
-let raw_sopattern_of_compattern sign com =
-  failwith "raw_sopattern_of_compattern: TODO"
-  (***
-  let c = Astterm.raw_constr_of_compattern Evd.empty (gLOB sign) com in
-  strong whd_replmeta c
-  ***)
+let raw_sopattern_of_compattern env com =
+  let c = Astterm.constr_of_com_pattern Evd.empty env com in
+  strong (fun _ _ -> whd_replmeta) env Evd.empty c
 
 let parse_pattern s =
   let com =
@@ -42,7 +39,7 @@ let parse_pattern s =
     with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
       error "Malformed pattern" 
   in
-  raw_sopattern_of_compattern (Global.context()) com
+  raw_sopattern_of_compattern (Global.env()) com
     
 let (pattern_stock : constr Stock.stock) =
   Stock.make_stock {name="PATTERN";proc=parse_pattern}
diff --git a/tactics/pattern.mli b/tactics/pattern.mli
index fc9d07ef7f..afe1ec848e 100644
--- a/tactics/pattern.mli
+++ b/tactics/pattern.mli
@@ -47,9 +47,7 @@ val put_pat            : module_mark -> string -> marked_term
 val get_pat            : marked_term -> constr
 val pattern_stock      : constr Stock.stock
 
-(*i**
-val raw_sopattern_of_compattern : typed_type signature -> CoqAst.t -> constr
-**i*)
+val raw_sopattern_of_compattern : Environ.env -> Coqast.t -> constr
 
 (*s Second part : Given a term with second-order variables in it,
    represented by Meta's, and possibly applied using \verb!XTRA[$SOAPP]! to
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6fb962f2cd..ff5d324a31 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -16,6 +16,7 @@ open Proof_trees
 open Clenv
 open Pattern
 open Wcclausenv
+open Pretty
 
 (******************************************)
 (*         Basic Tacticals                *)
@@ -197,7 +198,7 @@ let conclPattern concl pat tacast gl =
     List.map 
       (fun (i,c) -> (i, Termast.bdize false (assumptions_for_print []) c))
       constr_bindings in 
-  let tacast' = CoqAst.subst_meta ast_bindings tacast in
+  let tacast' = Coqast.subst_meta ast_bindings tacast in
     Tacinterp.interp tacast' gl
 ***)