In Pcoq, the search commands had an erroneous behavior. Bound variables

in theorems were renamed to avoid the names present in the current goal's
context.  This version corrects this problem.


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

4 files changed, 13 insertions, 11 deletions

diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml
index fd60e1e61f..1cd2070479 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml
@@ -252,7 +252,7 @@ let add_search (global_reference:global_reference) assumptions cstr =
 			global_reference) in
   let ast = 
     try
-      CT_premise (CT_ident id_string, translate_constr assumptions cstr)
+      CT_premise (CT_ident id_string, translate_constr false assumptions cstr)
     with Not_found ->
       CT_premise (CT_ident id_string,
                   CT_coerce_ID_to_FORMULA(
@@ -271,14 +271,14 @@ let ctf_EmptyGoalMessage id =
 let print_check (ast, judg) =
  let {uj_val=value; uj_type=typ} = judg in
  let value_ct_ast = 
-     (try translate_constr (Global.env()) value 
+     (try translate_constr false (Global.env()) value 
       with UserError(f,str) ->
            raise(UserError(f,
 			   Ast.print_ast 
 				(ast_of_constr true (Global.env()) value) ++
 			      fnl () ++ str ))) in
  let type_ct_ast =
-     (try translate_constr (Global.env()) typ
+     (try translate_constr false (Global.env()) typ
       with UserError(f,str) ->
            raise(UserError(f, Ast.print_ast (ast_of_constr true (Global.env())
 					       value) ++ fnl() ++ str))) in
@@ -300,8 +300,8 @@ and ntyp = nf_betaiota typ in
   (CT_premises_list
   [CT_eval_result
     (xlate_formula ast,
-    translate_constr env nvalue,
-    translate_constr env ntyp)]))));;
+    translate_constr false env nvalue,
+    translate_constr false env ntyp)]))));;
 
 
 
diff --git a/contrib/interface/showproof_ct.ml b/contrib/interface/showproof_ct.ml
index b689620e34..ee901c5e7c 100644
--- a/contrib/interface/showproof_ct.ml
+++ b/contrib/interface/showproof_ct.ml
@@ -52,7 +52,7 @@ let stde()  = (Global.env())
 ;;
 
 let spt t =
-   let f = (translate_constr (stde()) t) in
+   let f = (translate_constr true (stde()) t) in
    Hashtbl.add ct_FORMULA_constr f t;
    CT_text_formula f
 ;;
diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml
index c691ff912e..9d4d628044 100644
--- a/contrib/interface/translate.ml
+++ b/contrib/interface/translate.ml
@@ -108,8 +108,8 @@ let rec discard_coercions =
     | it -> it;;
 
 (*translates a formula into a centaur-tree --> FORMULA *)
-let translate_constr assumptions c =
- let com = ast_of_constr true assumptions c in
+let translate_constr at_top assumptions c =
+ let com = ast_of_constr at_top assumptions c in
 (* dead code:  let rcom = relativize_cci (discard_coercions com) in *)
  xlate_formula (Ctast.ast_to_ct com) (* dead code: rcom *);;
 
@@ -119,7 +119,7 @@ let translate_sign env =
   let l = 
     fold_named_context
       (fun env (id,v,c) l -> 
-	 (CT_premise(CT_ident(string_of_id id), translate_constr env c))::l)
+	 (CT_premise(CT_ident(string_of_id id), translate_constr false env c))::l)
       env ~init:[] 
   in
   CT_premises_list l;;
@@ -158,4 +158,4 @@ let translate_path l =
 
 (*translates a path and a goal into a centaur-tree --> RULE *)
 let translate_goal (g:goal) =
- CT_rule(translate_sign (evar_env g), translate_constr (evar_env g) g.evar_concl);;
+ CT_rule(translate_sign (evar_env g), translate_constr true (evar_env g) g.evar_concl);;
diff --git a/contrib/interface/translate.mli b/contrib/interface/translate.mli
index 46d785f4bf..65d8331b2d 100644
--- a/contrib/interface/translate.mli
+++ b/contrib/interface/translate.mli
@@ -5,5 +5,7 @@ open Environ;;
 open Term;;
 
 val translate_goal : goal -> ct_RULE;;
-val translate_constr : env -> constr -> ct_FORMULA;;
+(* The boolean argument indicates whether names from the environment should *)
+(*  be avoided (same interpretation as for prterm_env and ast_of_constr)    *)
+val translate_constr : bool -> env -> constr -> ct_FORMULA;;
 val translate_path : int list -> ct_SIGNED_INT_LIST;;