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, 2 insertions, 3 deletions

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