Réforme de l'interprétation des termes :

- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
  pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
  se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
  constrextern.ml est l'équivalent de termast.ml pour le nouveau
  printer; topconstr.ml; contient la définition de "constr_expr";
  modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid


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

19 files changed, 116 insertions, 216 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index ade0b02212..9c153b15e2 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -428,19 +428,19 @@ let add_hints dbnames h =
   let dbnames = if dbnames = [] then ["core"] else dbnames in match h with
   | HintsResolve lhints ->	
       let env = Global.env() and sigma = Evd.empty in
-      let f (n,c) = 
-	let c = Astterm.interp_constr sigma env c in
+      let f (n,c) =
+	let c = Constrintern.interp_constr sigma env c in
 	let n = match n with
-	  | None -> basename (sp_of_global None (Declare.reference_of_constr c))
+	  | None -> basename (sp_of_global None (reference_of_constr c))
 	  | Some n -> n in
 	(n,c) in
       add_resolves env sigma (List.map f lhints) dbnames
   | HintsImmediate lhints ->
       let env = Global.env() and sigma = Evd.empty in
       let f (n,c) = 
-	let c = Astterm.interp_constr sigma env c in
+	let c = Constrintern.interp_constr sigma env c in
 	let n = match n with
-	  | None -> basename (sp_of_global None (Declare.reference_of_constr c))
+	  | None -> basename (sp_of_global None (reference_of_constr c))
 	  | Some n -> n in
 	(n,c) in
       add_trivials env sigma (List.map f lhints) dbnames
@@ -460,7 +460,7 @@ let add_hints dbnames h =
       let lcons = List.map2 (fun id c -> (id,c)) (Array.to_list consnames) lcons in
       add_resolves env sigma lcons dbnames
   | HintsExtern (hintname, pri, patcom, tacexp) ->
-      let pat =	Astterm.interp_constrpattern Evd.empty (Global.env()) patcom in
+      let pat =	Constrintern.interp_constrpattern Evd.empty (Global.env()) patcom in
       add_externs hintname pri pat tacexp dbnames
 
 (**************************************************************************)
@@ -901,7 +901,7 @@ let default_superauto g = superauto !default_search_depth [] [] g
 let interp_to_add gl locqid =
   let r = Nametab.global locqid in
   let id = basename (sp_of_global None r) in
-  (next_ident_away id (pf_ids_of_hyps gl), Declare.constr_of_reference r)
+  (next_ident_away id (pf_ids_of_hyps gl), constr_of_reference r)
 
 let gen_superauto nopt l a b gl =
   let n = match nopt with Some n -> n | None -> !default_search_depth in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index c887c1bb49..4cd017e5f0 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -185,4 +185,4 @@ type autoArguments =
 val superauto : int -> (identifier * constr) list -> autoArguments list -> tactic
 *)
 
-val h_superauto : int option -> qualid located list -> bool -> bool -> tactic
+val h_superauto : int option -> reference list -> bool -> bool -> tactic
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index a000839380..419d9c43c9 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -128,10 +128,10 @@ open Tacticals
 open Libobject
 open Library
 open Pattern
-open Coqast
 open Ast
 open Pcoq
 open Tacexpr
+open Libnames
 
 (* two patterns - one for the type, and one for the type of the type *)
 type destructor_pattern = {
@@ -215,7 +215,7 @@ let add_destructor_hint na loc pat pri code =
 	  errorlabstrm "add_destructor_hint"
           (str "The tactic should be a function of the hypothesis name") end
   in
-  let (_,pat) = Astterm.interp_constrpattern Evd.empty (Global.env()) pat in
+  let (_,pat) = Constrintern.interp_constrpattern Evd.empty (Global.env()) pat in
   let pat = match loc with
     | HypLocation b ->
 	HypLocation
@@ -251,7 +251,7 @@ let applyDestructor cls discard dd gls =
     with PatternMatchingFailure -> error "No match" in
   let tac = match cls, dd.d_code with
     | Some id, (Some x, tac) -> 
-	let arg = Reference (RIdent (dummy_loc,id)) in
+	let arg = Reference (Ident (dummy_loc,id)) in
         TacLetIn ([(dummy_loc, x), None, arg], tac)
     | None, (None, tac) -> tac
     | _, (Some _,_) -> error "Destructor expects an hypothesis"
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index bedbb26c9e..2015f6053d 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.mli
@@ -27,4 +27,4 @@ val h_auto_tdb : int option -> tactic
 
 val add_destructor_hint :
   identifier -> (bool,unit) Tacexpr.location ->
-    Genarg.constr_ast -> int -> Tacexpr.raw_tactic_expr -> unit
+    Topconstr.constr_expr -> int -> Tacexpr.raw_tactic_expr -> unit
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 8ab6d23ab5..896218c804 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -45,11 +45,7 @@ let e_resolve_with_bindings_tac  (c,lbind) gl =
   let clause = make_clenv_binding_apply wc (-1) (c,t) lbind in 
   e_res_pf kONT clause gl
 
-let e_resolve_with_bindings = 
-  tactic_com_bind_list e_resolve_with_bindings_tac
-
 let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,NoBindings) gls
-let resolve_constr c gls = Tactics.apply_with_bindings (c,NoBindings) gls
 			     
 TACTIC EXTEND EExact
 | [ "EExact" constr(c) ] -> [ e_give_exact c ]
@@ -61,6 +57,7 @@ let registered_e_assumption gl =
   tclFIRST (List.map (fun id gl -> e_give_exact_constr (mkVar id) gl) 
               (pf_ids_of_hyps gl)) gl
 
+(* This automatically define h_eApply (among other things) *)
 TACTIC EXTEND EApply
   [ "EApply" constr_with_bindings(c) ] -> [ e_resolve_with_bindings_tac c ]
 END
diff --git a/tactics/elim.ml b/tactics/elim.ml
index b4f718fbda..09c176ac68 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -128,7 +128,7 @@ let decompose_or c gls =
     (fun (_,t) -> is_disjunction t)
     c gls
 
-let inj x = Rawterm.AN (Rawterm.dummy_loc,x)
+let inj x = Rawterm.AN x
 let h_decompose l c =
   Refiner.abstract_tactic
     (TacDecompose (List.map inj l,c)) (decompose_these c l)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index fdd02fe92e..bfa1baf83b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -372,7 +372,7 @@ let descend_then sigma env head dirn =
       let brl =
         List.map build_branch
           (interval 1 (Array.length mip.mind_consnames)) in
-      let ci = make_default_case_info env ind in
+      let ci = make_default_case_info env RegularStyle ind in
       mkCase (ci, p, head, Array.of_list brl)))
   
 (* Now we need to construct the discriminator, given a discriminable
@@ -420,7 +420,7 @@ let construct_discriminator sigma env dirn c sort =
     it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args in
   let brl =
     List.map build_branch(interval 1 (Array.length mip.mind_consnames)) in
-  let ci = make_default_case_info env ind in
+  let ci = make_default_case_info env RegularStyle ind in
   mkCase (ci, p, c, Array.of_list brl)
     
 let rec build_discriminator sigma env dirn c sort = function
@@ -556,12 +556,6 @@ let discr_tac = function
 let discrConcl gls  = discrClause None gls
 let discrHyp id gls = discrClause (Some id) gls
 
-(*
-let h_discr      = hide_atomic_tactic "Discr"      discrEverywhere
-let h_discrConcl = hide_atomic_tactic "DiscrConcl" discrConcl
-let h_discrHyp   = hide_ident_or_numarg_tactic "DiscrHyp" discrHyp
-*)
-
 (* returns the sigma type (sigS, sigT) with the respective
     constructor depending on the sort *)
 
@@ -811,11 +805,6 @@ let injClause = function
 let injConcl gls  = injClause None gls
 let injHyp id gls = injClause (Some id) gls
 
-(*
-let h_injConcl = hide_atomic_tactic "Inj" injConcl
-let h_injHyp   = hide_ident_or_numarg_tactic "InjHyp" injHyp
-*)
-
 let decompEqThen ntac id gls =
   let eqn = pf_whd_betadeltaiota gls (clause_type (Some id) gls) in
   let (lbeq,(t,t1,t2))= find_eq_data_decompose  eqn in
@@ -876,11 +865,6 @@ let dEq = dEqThen (fun x -> tclIDTAC)
 let dEqConcl gls = dEq None gls
 let dEqHyp id gls = dEq (Some id) gls
 
-(*
-let dEqConcl_tac = hide_atomic_tactic "DEqConcl" dEqConcl
-let dEqHyp_tac = hide_ident_or_numarg_tactic "DEqHyp" dEqHyp
-*)
-
 let rewrite_msg = function 
   | None ->  
       (str "passed term is not a primitive equality") 
@@ -1099,18 +1083,6 @@ let subst l2r eqn cls gls =
 
 let substConcl l2r eqn gls = try_rewrite (subst l2r eqn None) gls
 let substConcl_LR = substConcl true
-(*
-let substConcl_LR_tac = 
-  let gentac = 
-    hide_tactic "SubstConcl_LR"
-      (function 
-	 | [Command eqn] -> 
-	     (fun gls ->  substConcl_LR (pf_interp_constr gls eqn)  gls)
-	 | [Constr c] -> substConcl_LR c
-	 | _ -> assert false)
-  in 
-  fun eqn  -> gentac [Command eqn] 
-*)
 
 (* id:(P a) |- G
  * SubstHyp a=b id
@@ -1135,16 +1107,6 @@ let hypSubst_LR = hypSubst true
  *)
 let substHypInConcl l2r id gls = try_rewrite (hypSubst l2r id None) gls
 let substHypInConcl_LR = substHypInConcl true
-(*
-let substHypInConcl_LR_tac =
-  let gentac = 
-    hide_tactic "SubstHypInConcl_LR" 
-      (function 
-	 | [Identifier id] -> substHypInConcl_LR id
-	 | _ -> assert false)
-  in 
-  fun id -> gentac [Identifier id]
-*)
 
 (* id:a=b H:(P a) |- G
    SubstHypInHyp id H.
@@ -1156,18 +1118,6 @@ let substHypInConcl_LR_tac =
      |- a=b
 *)
 let substConcl_RL = substConcl false
-(*
-let substConcl_RL_tac = 
-  let gentac = 
-    hide_tactic "SubstConcl_RL"
-      (function 
-	 | [Command eqn] -> 
-	     (fun gls ->  substConcl_RL (pf_interp_constr gls eqn)  gls)
-         | [Constr c] -> substConcl_RL c
-	 | _ -> assert false)
-  in 
-  fun eqn  -> gentac [Command eqn] 
-*)
 
 (* id:(P b) |-G
    SubstHyp_RL a=b id 
@@ -1184,16 +1134,6 @@ let hypSubst_RL = hypSubst false
  * id:a=b |- (P a)
  *)
 let substHypInConcl_RL = substHypInConcl false
-(*
-let substHypInConcl_RL_tac =
-  let gentac = 
-    hide_tactic "SubstHypInConcl_RL" 
-      (function 
-	 | [Identifier id] -> substHypInConcl_RL id
-         | _ -> assert false)
-  in 
-  fun id -> gentac [Identifier id]
-*)
 
 (* id:a=b H:(P b) |- G
    SubstHypInHyp id H.
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index d5a2b98868..d90de63c94 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -11,11 +11,12 @@
 open Tacexpr
 open Term
 open Proof_type
+open Topconstr
 
 val rawwit_orient : bool raw_abstract_argument_type
 val wit_orient : bool closed_abstract_argument_type
 val orient : bool Pcoq.Gram.Entry.e
 
-val rawwit_with_constr : Coqast.t option raw_abstract_argument_type
+val rawwit_with_constr : constr_expr option raw_abstract_argument_type
 val wit_with_constr : constr option closed_abstract_argument_type
-val with_constr : Coqast.t option Pcoq.Gram.Entry.e
+val with_constr : constr_expr option Pcoq.Gram.Entry.e
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 6907acd355..2d89b84f56 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -132,7 +132,7 @@ END
 
 let add_rewrite_hint name ort t lcsr =
   let env = Global.env() and sigma = Evd.empty in
-  let f c = Astterm.interp_constr sigma env c, ort, t in
+  let f c = Constrintern.interp_constr sigma env c, ort, t in
   add_rew_rules name (List.map f lcsr)
 
 VERNAC COMMAND EXTEND HintRewrite
@@ -171,10 +171,6 @@ VERNAC COMMAND EXTEND AddSetoid
 | [ "Add" "Morphism" constr(m) ":" ident(s) ] -> [ new_named_morphism s m ]
 END
 
-(*
-cp tactics/extratactics.ml4 toto.ml; camlp4o -I parsing pa_extend.cmo grammar.cma pr_o.cmo toto.ml 
-*)
-
 (* Inversion lemmas (Leminv) *)
 
 VERNAC COMMAND EXTEND DeriveInversionClear
@@ -188,15 +184,18 @@ VERNAC COMMAND EXTEND DeriveInversionClear
   -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
 
 | [ "Derive" "Inversion_clear"  ident(na) "with" constr(c) ]
-  -> [ add_inversion_lemma_exn na c (let loc = (0,0) in <:ast< (PROP) >>) false inv_clear_tac ]
+  -> [ add_inversion_lemma_exn na c (Rawterm.RProp Term.Null) false inv_clear_tac ]
 END
 
+open Term
+open Rawterm
+
 VERNAC COMMAND EXTEND DeriveInversion
 | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
   -> [ add_inversion_lemma_exn na c s false half_inv_tac ]
 
 | [ "Derive" "Inversion" ident(na) "with" constr(c) ]
-  -> [ add_inversion_lemma_exn na c (let loc = (0,0) in <:ast< (PROP) >>) false half_inv_tac ]
+  -> [ add_inversion_lemma_exn na c (RProp Null) false half_inv_tac ]
 
 | [ "Derive" "Inversion" ident(na) ident(id) ]
   -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false half_inv_tac ]
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 1fcf1e6bd0..75bcb0d6be 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -61,7 +61,7 @@ let h_specialize n (c,bl as d) =
 let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c)
 
 (* Context management *)
-let inj x = AN (Rawterm.dummy_loc,x)
+let inj x = AN x
 let h_clear l = abstract_tactic (TacClear (List.map inj l)) (clear l)
 let h_clear_body l =
   abstract_tactic (TacClearBody (List.map inj l)) (clear_body l)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index adc2054fe2..6edf56017b 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -274,8 +274,8 @@ let inversion_lemma_from_goal n na id sort dep_option inv_op =
    
 let add_inversion_lemma_exn na com comsort bool tac =
   let env = Global.env () and sigma = Evd.empty in
-  let c = Astterm.interp_type sigma env com in
-  let sort = Astterm.interp_sort comsort in
+  let c = Constrintern.interp_type sigma env com in
+  let sort = Pretyping.interp_sort comsort in
   try
     add_inversion_lemma na env sigma c sort bool tac
   with 
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 3d5f33c66a..17e1b05526 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -3,6 +3,7 @@ open Names
 open Term
 open Rawterm
 open Proof_type
+open Topconstr
 
 val lemInv_gen : quantified_hypothesis -> constr -> tactic
 val lemInvIn_gen : quantified_hypothesis -> constr -> identifier list -> tactic
@@ -11,5 +12,5 @@ val inversion_lemma_from_goal :
   int -> identifier -> identifier -> sorts -> bool ->
     (identifier -> tactic) -> unit
 val add_inversion_lemma_exn :
-  identifier -> Coqast.t -> Coqast.t -> bool -> (identifier -> tactic) -> unit
+  identifier -> constr_expr -> rawsort -> bool -> (identifier -> tactic) -> unit
 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 3a4ae8e13b..fa62c8dd46 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -45,7 +45,7 @@ type morphism =
       lem2 : constr option
     }
 
-let constr_of c = Astterm.interp_constr Evd.empty (Global.env()) c
+let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
 
 let constant dir s =
   let dir = make_dirpath
@@ -414,9 +414,8 @@ let new_morphism m id hook =
 	let args_t = (List.map snd args) in
 	let poss = (List.map setoid_table_mem args_t) in
 	let lem = (gen_compat_lemma env m body args_t poss) in
-	let lemast = (ast_of_constr true env lem) in
 	new_edited id m poss;
-	start_proof_com (Some id) (IsGlobal DefinitionBody) ([],lemast) hook;
+	start_proof id (IsGlobal DefinitionBody) lem hook;
 	(Options.if_verbose Vernacentries.show_open_subgoals ()))
 
 let rec sub_bool l1 n = function
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index d8bc556562..e4d49e9029 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -10,7 +10,7 @@
 
 open Term
 open Proof_type
-open Genarg
+open Topconstr
 
 val equiv_list : unit -> constr list
 
@@ -22,6 +22,6 @@ val setoid_rewriteRL : constr -> tactic
 
 val general_s_rewrite : bool -> constr -> tactic
 
-val add_setoid : constr_ast -> constr_ast -> constr_ast -> unit
+val add_setoid : constr_expr -> constr_expr -> constr_expr -> unit
 
-val new_named_morphism : Names.identifier -> constr_ast -> unit
+val new_named_morphism : Names.identifier -> constr_expr -> unit
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index efa497b951..be6362d3a9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-open Astterm
+open Constrintern
 open Closure
 open RedFlags
 open Declarations
@@ -30,7 +30,7 @@ open Proof_type
 open Refiner
 open Tacmach
 open Tactic_debug
-open Coqast
+open Topconstr
 open Ast
 open Term
 open Termops
@@ -63,7 +63,7 @@ type value =
   | VFTactic of value list * (value list->tactic)
   | VRTactic of (goal list sigma * validation)
   | VContext of interp_sign * direction_flag
-      * (pattern_ast,raw_tactic_expr) match_rule list
+      * (pattern_expr,raw_tactic_expr) match_rule list
   | VFun of (identifier * value) list * identifier option list *raw_tactic_expr
   | VVoid
   | VInteger of int
@@ -165,9 +165,6 @@ let valueOut = function
     anomalylabstrm "valueOut"
       (str "Not a Dynamic ast: " (* ++ print_ast ast*) )
 
-let constrIn c = constrIn c
-let constrOut = constrOut
-
 let loc = dummy_loc
 
 (* Table of interpretation functions *)
@@ -297,7 +294,7 @@ let glob_hyp (lfun,_) (loc,id) =
 *)
     Pretype_errors.error_var_not_found_loc loc id
 
-let glob_lochyp ist (loc,_ as locid) = (loc,glob_hyp ist locid)
+let glob_lochyp ist (_loc,_ as locid) = (loc,glob_hyp ist locid)
 
 let error_unbound_metanum loc n =
   user_err_loc
@@ -307,30 +304,25 @@ let glob_metanum ist loc n =
   if List.mem n (snd ist) then n else error_unbound_metanum loc n
 
 let glob_hyp_or_metanum ist = function
-  | AN (loc,id) -> AN (loc,glob_hyp ist (loc,id))
-  | MetaNum (loc,n) -> MetaNum (loc,glob_metanum ist loc n)
+  | AN id -> AN (glob_hyp ist (loc,id))
+  | MetaNum (_loc,n) -> MetaNum (loc,glob_metanum ist loc n)
 
 let glob_qualid_or_metanum ist = function
-  | AN (loc,qid) -> AN (loc,qualid_of_sp (sp_of_global None (Nametab.global (loc,qid))))
-  | MetaNum (loc,n) -> MetaNum (loc,glob_metanum ist loc n)
+  | AN qid -> AN (Qualid(loc,qualid_of_sp (sp_of_global None (Nametab.global qid))))
+  | MetaNum (_loc,n) -> MetaNum (loc,glob_metanum ist loc n)
 
-let glob_reference ist (_,qid as locqid) =
-  let dir, id = repr_qualid qid in
-  try 
-    if dir = empty_dirpath && List.mem id (fst ist) then qid
-    else raise Not_found
-  with Not_found ->
-    qualid_of_sp (sp_of_global None (Nametab.global locqid))
+let glob_reference ist = function
+  | Ident (loc,id) as r when List.mem id (fst ist) -> r
+  | r -> Qualid (loc,qualid_of_sp (sp_of_global None (Nametab.global r)))
 
-let glob_ltac_qualid ist (loc,qid as locqid) =
-  try qualid_of_sp (locate_tactic qid)
-  with Not_found -> glob_reference ist locqid
+let glob_ltac_qualid ist ref =
+  let (loc,qid) = qualid_of_reference ref in
+  try Qualid (loc,qualid_of_sp (locate_tactic qid))
+  with Not_found -> glob_reference ist ref
 
 let glob_ltac_reference ist = function
-  | RIdent (loc,id) -> 
-      if List.mem id (fst ist) then RIdent (loc,id)
-      else RQualid (loc,glob_ltac_qualid ist (loc,make_short_qualid id))
-  | RQualid qid -> RQualid (loc,glob_ltac_qualid ist qid)
+  | Ident (_loc,id) when List.mem id (fst ist) -> Ident (loc,id)
+  | r -> glob_ltac_qualid ist r
 
 let rec glob_intro_pattern lf ist = function
   | IntroOrAndPattern l ->
@@ -346,8 +338,10 @@ let glob_quantified_hypothesis ist x =
   x
 
 let glob_constr ist c =
-  let _ = Astterm.interp_rawconstr_gen Evd.empty (Global.env()) [] false (fst ist) c in
-  c
+  let _ =
+    Constrintern.interp_rawconstr_gen
+      Evd.empty (Global.env()) [] false (fst ist) c
+  in c
 
 (* Globalize bindings *)
 let glob_binding ist (b,c) =
@@ -364,7 +358,7 @@ let glob_constr_with_bindings ist (c,bl) =
 let glob_clause_pattern ist (l,occl) =
   let rec check = function
     | (hyp,l) :: rest -> 
-	let (loc,_ as id) = skip_metaid hyp in
+	let (_loc,_ as id) = skip_metaid hyp in
 	(AI(loc,glob_hyp ist id),l)::(check rest)
     | [] -> []
   in (l,check occl)
@@ -372,12 +366,12 @@ let glob_clause_pattern ist (l,occl) =
 let glob_induction_arg ist = function
   | ElimOnConstr c -> ElimOnConstr (glob_constr ist c)
   | ElimOnAnonHyp n as x -> x
-  | ElimOnIdent (loc,id) as x -> x
+  | ElimOnIdent (_loc,id) as x -> ElimOnIdent (loc,id)
 
 (* Globalize a reduction expression *)
 let glob_evaluable_or_metanum ist = function
-  | AN (loc,qid) -> AN (loc,glob_reference ist (loc,qid))
-  | MetaNum (loc,n) -> MetaNum (loc,glob_metanum ist loc n)
+  | AN qid -> AN (glob_reference ist qid)
+  | MetaNum (_loc,n) -> MetaNum (loc,glob_metanum ist loc n)
 
 let glob_unfold ist (l,qid) = (l,glob_evaluable_or_metanum ist qid)
 
@@ -398,10 +392,10 @@ let glob_redexp ist = function
 (* Interprets an hypothesis name *)
 let glob_hyp_location ist = function
   | InHyp id ->
-      let (loc,_ as id) = skip_metaid id in
+      let (_loc,_ as id) = skip_metaid id in
       InHyp (AI(loc,glob_hyp ist id))
   | InHypType id -> 
-      let (loc,_ as id) = skip_metaid id in
+      let (_loc,_ as id) = skip_metaid id in
       InHypType (AI(loc,glob_hyp ist id))
 
 (* Reads a pattern *)
@@ -465,7 +459,7 @@ let rec glob_atomic lf ist = function
   | TacIntrosUntil hyp -> TacIntrosUntil (glob_quantified_hypothesis ist hyp)
   | TacIntroMove (ido,ido') ->
       TacIntroMove (option_app (glob_ident lf ist) ido,
-          option_app (fun (loc,_ as x) -> (loc,glob_hyp ist x)) ido')
+          option_app (fun (_loc,_ as x) -> (loc,glob_hyp ist x)) ido')
   | TacAssumption -> TacAssumption
   | TacExact c -> TacExact (glob_constr ist c)
   | TacApply cb -> TacApply (glob_constr_with_bindings ist cb)
@@ -497,7 +491,7 @@ let rec glob_atomic lf ist = function
   | TacTrivial l -> TacTrivial l
   | TacAuto (n,l) -> TacAuto (n,l)
   | TacAutoTDB n -> TacAutoTDB n
-  | TacDestructHyp (b,(loc,_ as id)) -> TacDestructHyp(b,(loc,glob_hyp ist id))
+  | TacDestructHyp (b,(_loc,_ as id)) -> TacDestructHyp(b,(loc,glob_hyp ist id))
   | TacDestructConcl -> TacDestructConcl
   | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
   | TacDAuto (n,p) -> TacDAuto (n,p)
@@ -550,15 +544,15 @@ let rec glob_atomic lf ist = function
   | TacTransitivity c -> TacTransitivity (glob_constr ist c)
 
   (* For extensions *)
-  | TacExtend (opn,l) ->
+  | TacExtend (_loc,opn,l) ->
       let _ = lookup_tactic opn in
-      TacExtend (opn,List.map (glob_genarg ist) l)
+      TacExtend (loc,opn,List.map (glob_genarg ist) l)
   | TacAlias (_,l,body) -> failwith "TacAlias globalisation: TODO"
 
 and glob_tactic ist tac = snd (glob_tactic_seq ist tac)
 
 and glob_tactic_seq (lfun,lmeta as ist) = function
-  | TacAtom (loc,t) ->
+  | TacAtom (_loc,t) ->
       let lf = ref lfun in
       let t = glob_atomic lf ist t in
       !lf, TacAtom (loc, t)
@@ -612,10 +606,10 @@ and glob_tacarg ist = function
   | Reference r -> Reference (glob_ltac_reference ist r)
   | Integer n -> Integer n
   | ConstrMayEval c -> ConstrMayEval (glob_constr_may_eval ist c)
-  | MetaNumArg (loc,n) -> MetaNumArg (loc,glob_metanum ist loc n)
-  | MetaIdArg (loc,_) -> error_syntactic_metavariables_not_allowed loc
-  | TacCall (loc,f,l) ->
-      TacCall (loc,glob_ltac_reference ist f,List.map (glob_tacarg ist) l)
+  | MetaNumArg (_loc,n) -> MetaNumArg (loc,glob_metanum ist loc n)
+  | MetaIdArg (_loc,_) -> error_syntactic_metavariables_not_allowed loc
+  | TacCall (_loc,f,l) ->
+      TacCall (_loc,glob_ltac_reference ist f,List.map (glob_tacarg ist) l)
   | Tacexp t -> Tacexp (glob_tactic ist t)
   | TacDynamic(_,t) as x ->
       (match tag t with
@@ -641,7 +635,7 @@ and glob_genarg ist x =
   | IntArgType -> in_gen rawwit_int (out_gen rawwit_int x)
   | IntOrVarArgType ->
       let f = function
-	| ArgVar (loc,id) -> ArgVar (loc,glob_hyp ist (loc,id))
+	| ArgVar (_loc,id) -> ArgVar (loc,glob_hyp ist (loc,id))
 	| ArgArg n as x -> x in
       in_gen rawwit_int_or_var (f (out_gen rawwit_int_or_var x))
   | StringArgType ->
@@ -650,9 +644,10 @@ and glob_genarg ist x =
       in_gen rawwit_pre_ident (out_gen rawwit_pre_ident x)
   | IdentArgType ->
       in_gen rawwit_ident (glob_hyp ist (dummy_loc,out_gen rawwit_ident x))
-  | QualidArgType ->
-      let (loc,qid) = out_gen rawwit_qualid x in
-      in_gen rawwit_qualid (loc,glob_ltac_qualid ist (loc,qid))
+  | RefArgType ->
+      in_gen rawwit_ref (glob_ltac_reference ist (out_gen rawwit_ref x))
+  | SortArgType ->
+      in_gen rawwit_sort (out_gen rawwit_sort x)
   | ConstrArgType ->
       in_gen rawwit_constr (glob_constr ist (out_gen rawwit_constr x))
   | ConstrMayEvalArgType ->
@@ -679,29 +674,6 @@ and glob_genarg ist x =
 
 (************* END GLOBALIZE ************)
 
-(* Reads the head of Fun *)
-let read_fun ast =
-  let rec read_fun_rec = function
-    | Node(_,"VOID",[])::tl -> None::(read_fun_rec tl)
-    | Nvar(_,s)::tl -> (Some s)::(read_fun_rec tl)
-    | [] -> []
-    | _ ->
-      anomalylabstrm "Tacinterp.read_fun_rec" (str "Fun not well formed")
-  in
-    match ast with
-      | Node(_,"FUNVAR",l) -> read_fun_rec l
-      | _ ->
-        anomalylabstrm "Tacinterp.read_fun" (str "Fun not well formed")
-
-(* Reads the clauses of a Rec *)
-let rec read_rec_clauses = function
-  | [] -> []
-  | Node(_,"RECCLAUSE",[Nvar(_,name);it;body])::tl ->
-    (name,it,body)::(read_rec_clauses tl)
-  |_ ->
-    anomalylabstrm "Tacinterp.read_rec_clauses"
-      (str "Rec not well formed")
-
 (* Associates variables with values and gives the remaining variables and
    values *)
 let head_with_value (lvar,lval) =
@@ -906,7 +878,7 @@ let name_interp ist = function
   | Name id -> Name (ident_interp ist id)
 
 let hyp_or_metanum_interp ist = function
-  | AN (loc,id) -> ident_interp ist id
+  | AN id -> ident_interp ist id
   | MetaNum (loc,n) -> constr_to_id loc (List.assoc n ist.lmatch)
 
 (* To avoid to move to much simple functions in the big recursive block *)
@@ -924,32 +896,30 @@ let interp_ltac_qualid is_applied ist (loc,qid as lqid) =
   with Not_found -> interp_pure_qualid is_applied ist lqid
 
 let interp_ltac_reference isapplied ist = function
-  | RIdent (loc,id) -> 
+  | Ident (loc,id) -> 
       (try unrec (List.assoc id ist.lfun)
       with | Not_found ->
         interp_ltac_qualid isapplied ist (loc,make_short_qualid id))
-  | RQualid qid -> interp_ltac_qualid isapplied ist qid
+  | Qualid qid -> interp_ltac_qualid isapplied ist qid
 
 (* Interprets a qualified name *)
-let eval_qualid ist (loc,qid as locqid) =
-  let dir, id = repr_qualid qid in
-  try 
-    if dir = empty_dirpath then unrec (List.assoc id ist.lfun) 
-    else raise Not_found
-  with | Not_found ->
-    interp_pure_qualid false ist locqid
-
-let qualid_interp ist qid =
-  let v = eval_qualid ist qid in
+let eval_ref ist = function
+  | Qualid locqid -> interp_pure_qualid false ist locqid
+  | Ident (loc,id) ->
+      try unrec (List.assoc id ist.lfun)
+      with Not_found -> interp_pure_qualid false ist (loc,make_short_qualid id)
+
+let reference_interp ist qid =
+  let v = eval_ref ist qid in
   coerce_to_reference ist v
 
 (* Interprets a qualified name. This can be a metavariable to be injected *)
 let qualid_or_metanum_interp ist = function
-  | AN (loc,qid) -> qid
+  | AN qid -> qid
   | MetaNum (loc,n) -> constr_to_qid loc (List.assoc n ist.lmatch)
 
 let eval_ref_or_metanum ist = function
-  | AN (loc,qid) -> eval_qualid ist (loc,qid)
+  | AN qid -> eval_ref ist qid
   | MetaNum (loc,n) -> VConstr (List.assoc n ist.lmatch)
 
 let interp_evaluable_or_metanum ist c =
@@ -1080,7 +1050,8 @@ let interp_induction_arg ist = function
       | Some gl ->
 	  if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
 	  else ElimOnConstr
-	    (constr_interp ist (Termast.ast_of_qualid (make_short_qualid id)))
+(*	    (constr_interp ist (Termast.ast_of_qualid (make_short_qualid id)))*)
+	    (constr_interp ist (CRef (Ident (loc,id))))
 
 let binding_interp ist (b,c) =
   (interp_quantified_hypothesis ist b,constr_interp ist c)
@@ -1174,12 +1145,6 @@ and tacarg_interp ist = function
 (*
   | Tacexp t -> VArg (Tacexp ((*tactic_interp ist t,*)t))
 *)
-(*
-    | Node(loc,s,l) ->
-        let fv = val_interp ist (Node(loc,"PRIMTACTIC",[Node(loc,s,[])]))
-        and largs = List.map (val_interp ist) l in
-        app_interp ist fv largs ast
-*)
   | TacDynamic(_,t) ->
       let tg = (tag t) in
       if tg = "tactic" then
@@ -1282,10 +1247,10 @@ and letin_interp ist = function
          by t;
          let (_,({const_entry_body = pft; const_entry_type = _},_,_)) =
            cook_proof () in
-         delete_proof id;
+         delete_proof (dummy_loc,id);
          (id,VConstr (mkCast (pft,typ)))::(letin_interp ist tl)
        with | NotTactic ->
-         delete_proof id;
+         delete_proof (dummy_loc,id);
          errorlabstrm "Tacinterp.letin_interp"
          (str "Term or fully applied tactic expected in Let"))
 
@@ -1329,7 +1294,7 @@ and letcut_interp ist = function
          by t;
          let (_,({const_entry_body = pft; const_entry_type = _},_,_)) =
            cook_proof () in
-         delete_proof id;
+         delete_proof (dummy_loc,id);
          let cutt = h_cut typ
          and exat = h_exact pft in
          tclTHENSV cutt [|tclTHEN (introduction id)
@@ -1340,7 +1305,7 @@ and letcut_interp ist = function
          tclTHEN ntac (tclTHEN (introduction id)
          (letcut_interp ist tl))*)
        with | NotTactic ->
-         delete_proof id;
+         delete_proof (dummy_loc,id);
          errorlabstrm "Tacinterp.letcut_interp"
          (str "Term or fully applied tactic expected in Let")))
 
@@ -1478,8 +1443,12 @@ and genarg_interp ist x =
       in_gen wit_pre_ident (out_gen rawwit_pre_ident x)
   | IdentArgType ->
       in_gen wit_ident (ident_interp ist (out_gen rawwit_ident x))
-  | QualidArgType ->
-      in_gen wit_qualid (qualid_interp ist (out_gen rawwit_qualid x))
+  | RefArgType ->
+      in_gen wit_ref (reference_interp ist (out_gen rawwit_ref x))
+  | SortArgType ->
+      in_gen wit_sort
+        (destSort 
+	  (constr_interp ist (CSort (dummy_loc,out_gen rawwit_sort x))))
   | ConstrArgType ->
       in_gen wit_constr (constr_interp ist (out_gen rawwit_constr x))
   | ConstrMayEvalArgType ->
@@ -1692,17 +1661,17 @@ and interp_atomic ist = function
   | TacTransitivity c -> h_transitivity (constr_interp ist c)
 
   (* For extensions *)
-  | TacExtend (opn,l) -> vernac_tactic (opn,List.map (genarg_interp ist) l)
+  | TacExtend (loc,opn,l) -> vernac_tactic (opn,List.map (genarg_interp ist) l)
   | TacAlias (_,l,body) ->
       let f x = match genarg_tag x with
   | IdentArgType -> VIdentifier (ident_interp ist (out_gen rawwit_ident x))
-  | QualidArgType -> VConstr (constr_of_reference (qualid_interp ist (out_gen rawwit_qualid x)))
+  | RefArgType -> VConstr (constr_of_reference (reference_interp ist (out_gen rawwit_ref x)))
   | ConstrArgType -> VConstr (constr_interp ist (out_gen rawwit_constr x))
   | ConstrMayEvalArgType ->
       VConstr (constr_interp_may_eval ist (out_gen rawwit_constr_may_eval x))
   | _ -> failwith "This generic type is not supported in alias" in
 
-      tactic_of_value (val_interp { ist with lfun=(List.map (fun (x,c) -> (id_of_string x,f c)) l)@ist.lfun } body)
+      tactic_of_value (val_interp { ist with lfun=(List.map (fun (x,c) -> (x,f c)) l)@ist.lfun } body)
 
 let _ = forward_vcontext_interp := vcontext_interp
  
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index c4017fc889..07ccf1d591 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -18,6 +18,7 @@ open Tactic_debug
 open Term
 open Tacexpr
 open Genarg
+open Topconstr
 (*i*)
 
 (* Values for interpretation *)
@@ -27,7 +28,7 @@ type value =
   | VFTactic of value list * (value list->tactic)
   | VRTactic of (goal list sigma * validation)
   | VContext of interp_sign * direction_flag
-      * (pattern_ast,raw_tactic_expr) match_rule list
+      * (pattern_expr,raw_tactic_expr) match_rule list
   | VFun of (identifier * value) list * identifier option list *raw_tactic_expr
   | VVoid
   | VInteger of int
@@ -59,9 +60,6 @@ val tacticIn : (interp_sign -> raw_tactic_expr) -> raw_tactic_expr
 val tacticOut : raw_tactic_expr -> (interp_sign -> raw_tactic_expr)
 val valueIn : value -> raw_tactic_arg
 val valueOut: raw_tactic_arg -> value
-val constrIn : constr -> Coqast.t
-val constrOut : Coqast.t -> constr
-val loc : Coqast.loc
 
 (* Sets the debugger mode *)
 val set_debug : debug_info -> unit
@@ -97,7 +95,7 @@ val tac_interp : (identifier * value) list -> (int * constr) list ->
                  debug_info -> raw_tactic_expr -> tactic
 
 (* Interprets constr expressions *)
-val constr_interp : interp_sign -> constr_ast -> constr
+val constr_interp : interp_sign -> constr_expr -> constr
 
 (* Initial call for interpretation *)
 val interp : raw_tactic_expr -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 25ba260d43..7a2014ae13 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -224,8 +224,8 @@ let reduce redexp cl goal =
 (* Unfolding occurrences of a constant *)
 
 let unfold_constr = function 
-  | ConstRef sp -> unfold_in_concl [[],Closure.EvalConstRef sp]
-  | VarRef id -> unfold_in_concl [[],Closure.EvalVarRef id]
+  | ConstRef sp -> unfold_in_concl [[],EvalConstRef sp]
+  | VarRef id -> unfold_in_concl [[],EvalVarRef id]
   | _ -> errorlabstrm "unfold_constr" (str "Cannot unfold a non-constant.")
 
 (*******************************************)
@@ -481,7 +481,6 @@ let apply_with_bindings (c,lbind) gl =
 
 
 let apply c = apply_with_bindings (c,NoBindings)
-let apply_com = tactic_com (fun c -> apply_with_bindings (c,NoBindings))
 
 let apply_list = function 
   | c::l -> apply_with_bindings (c,ImplicitBindings l)
@@ -494,8 +493,6 @@ let apply_without_reduce c gl =
   let clause = mk_clenv_type_of wc c in 
   res_pf kONT clause gl
 
-let apply_without_reduce_com = tactic_com  apply_without_reduce
-
 let refinew_scheme kONT clause gl = res_pf kONT clause gl
 
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
@@ -750,7 +747,7 @@ let exact_no_check = refine
 
 let exact_proof c gl =
   (* on experimente la synthese d'ise dans exact *)
-  let c = Astterm.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl)
+  let c = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl)
   in refine c gl 
 
 let (assumption : tactic) = fun gl ->
@@ -1638,7 +1635,7 @@ let abstract_subproof name tac gls =
     let cd = Entries.DefinitionEntry const in
     let sp = Declare.declare_constant na (cd,IsProof Lemma) in
     let newenv = Global.env() in
-    Declare.constr_of_reference (ConstRef (snd sp))
+    constr_of_reference (ConstRef (snd sp))
   in
   exact_no_check 
     (applist (lemme,
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index ce31a4dcc7..2e35c1761c 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -96,7 +96,7 @@ val try_intros_until :
 val assumption         : tactic
 val exact_no_check      : constr -> tactic
 val exact_check      : constr -> tactic
-val exact_proof      : Coqast.t -> tactic
+val exact_proof      : Topconstr.constr_expr -> tactic
 
 (*s Reduction tactics. *)
 
@@ -121,12 +121,11 @@ val simpl_option      : hyp_location option -> tactic
 val normalise_in_concl: tactic
 val normalise_in_hyp  : hyp_location        -> tactic
 val normalise_option  : hyp_location option -> tactic
-val unfold_in_concl   : (int list * Closure.evaluable_global_reference) list
-  -> tactic
+val unfold_in_concl   : (int list * evaluable_global_reference) list -> tactic
 val unfold_in_hyp     : 
-  (int list * Closure.evaluable_global_reference) list -> hyp_location -> tactic
+  (int list * evaluable_global_reference) list -> hyp_location -> tactic
 val unfold_option     : 
-  (int list * Closure.evaluable_global_reference) list -> hyp_location option
+  (int list * evaluable_global_reference) list -> hyp_location option
     -> tactic
 val reduce            : red_expr -> hyp_location list -> tactic
 val change            : constr -> hyp_location list -> tactic
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index dc28eb48cd..7e6334bc9a 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo" i*)
+(*i camlp4deps: "parsing/grammar.cma" i*)
 
 (*i $Id$ i*)