From bef4e9e5842527ffc76c0ae9635a2188fd09602a Mon Sep 17 00:00:00 2001
From: bertot
Date: Wed, 23 Jan 2002 14:17:57 +0000
Subject: 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
---
 contrib/interface/translate.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'contrib/interface/translate.ml')

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);;
-- 
cgit v1.2.3