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

1 files changed, 3 insertions, 3 deletions

diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index a00083938..419d9c43c 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"