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, 4 insertions, 7 deletions

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,