From a9f6f227bb6d51edce4293aaa013d543308282a3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 28 Apr 2000 19:24:57 +0000
Subject: Renommage bdize -> ast_of_constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@385 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof_trees.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index a9c65d50c4..f4990659c6 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -432,14 +432,15 @@ let ast_of_cvt_arg = function
   | Integer n       -> num n 
   | Command c       -> ope ("COMMAND",[c])
   | Constr  c       -> 
-      ope ("COMMAND",[bdize false (assumptions_for_print []) c])
+      ope ("COMMAND",[ast_of_constr false (assumptions_for_print []) c])
   | Clause idl      -> ope ("CLAUSE", List.map (compose nvar string_of_id) idl)
   | Bindings bl     -> ope ("BINDINGS", 
 			    List.map (ast_of_cvt_bind (fun x -> x)) bl)
   | Cbindings bl    -> 
       ope ("BINDINGS", 
 	   List.map 
-	     (ast_of_cvt_bind (bdize false (assumptions_for_print []))) bl)
+	     (ast_of_cvt_bind
+		(ast_of_constr false (assumptions_for_print []))) bl)
   | Tacexp ast      -> ope ("TACTIC",[ast]) 
   | Redexp (s,args) -> ope ("REDEXP", [ope(s,args)])
   | Fixexp (id,n,c) -> ope ("FIXEXP",[(nvar (string_of_id id)); 
-- 
cgit v1.2.3