Prsing

- Typage renforcé dans les grammaires (distinction des vars et des metavars)
- Disparition de SLAM au profit de ABSTRACT
- Paths primitifs dans les quotations (syntaxe concrète à base de .)
- Mise en place de identifier dès le type ast
- Protection de identifier contre les effets de bord via un String.copy
- Utilisation de module_ident (= identifier) dans les dir_path (au
  lieu de string)

Table des noms qualifiés

- Remplacement de la table de visibilité par une table qui ne cache
  plus les noms de modules et sections mais seulement les noms des
  constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel
  module A déjà existant : seuls les noms de constructions de l'ancien
  A qui existent aussi dans le nouveau A seront cachés)
- Renoncement à la possibilité d'accéder les formes non déchargées des
  constantes définies à l'intérieur de sections et simplification
  connexes (suppression de END-SECTION, une seule table de noms qui ne
  survit pas au discharge)
- Utilisation de noms longs pour les modules, de noms qualifiés pour
  Require and co, tests de cohérence; pour être cohérent avec la non
  survie des tables de noms à la sortie des section, les require à
  l'intérieur d'une section eux aussi sont refaits à la fermeture de la
  section


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

1 files changed, 6 insertions, 6 deletions

diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index c26a8039d..f84fe33ef 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -11,7 +11,7 @@ open Tactics;;
 open Tacticals;;
 open Pattern;;
 open Reduction;;
-open Coqast;;
+open Ctast;;
 open Termast;;
 open Astterm;;
 open Vernacinterp;;
@@ -36,10 +36,10 @@ open Paths;;
 *)
 
 
-type dad_rule = Coqast.t * int list * int list * int * int list * Coqast.t;;
+type dad_rule = Ctast.t * int list * int list * int * int list * Ctast.t;;
 
 (* This value will be used systematically when constructing objects of
-   type Coqast.t, the value is stupid and meaningless, but it is needed
+   type Ctast.t, the value is stupid and meaningless, but it is needed
    to construct well-typed terms. *)
 
 let zz = (0,0);;
@@ -66,7 +66,7 @@ let map_subst (env :env)
    let rec map_subst_aux = function
     Node(_, "META", [Num(_, i)]) ->
       let constr = List.assoc i subst in
-      ast_of_constr false env constr
+      Ctast.ast_to_ct (ast_of_constr false env constr)
   | Node(loc, s, l) -> Node(loc, s, List.map map_subst_aux l)
   | ast -> ast in
     map_subst_aux;;
@@ -89,7 +89,7 @@ let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 =
                 Failure s -> failwith "internal" in
          let _, constr_pat = 
             interp_constrpattern Evd.empty (Global.env())
-               pat in
+               (ct_to_ast pat) in
          let subst = matches constr_pat term_to_match in
          if (is_prefix p_f (p_r@p1)) & (is_prefix p_l (p_r@p2)) then
            map_subst env subst cmd
@@ -251,7 +251,7 @@ vinterp_add "AddDadRule"
              VARG_NUMBERLIST p2; VARG_TACTIC com] ->
             (function () ->
               let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in
-              (add_dad_rule name pat p1 p2 (List.length pr) pr com))
+              (add_dad_rule name (Ctast.ast_to_ct pat) p1 p2 (List.length pr) pr (Ctast.ast_to_ct com)))
             | _ -> errorlabstrm "AddDadRule1"
                     [< 'sTR "AddDadRule2">]);
 add_dad_rule "distributivity-inv"