From f454cc6dff2eadd720c126b8b43dff032efdb129 Mon Sep 17 00:00:00 2001
From: coq
Date: Thu, 21 Apr 2005 14:34:19 +0000
Subject: Gestion du forall et envoie d'axiome à la procédure

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6950 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/dp/dp_simplify.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'contrib/dp/dp_simplify.ml')

diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml
index 35c80e72a1..c330b9617d 100644
--- a/contrib/dp/dp_simplify.ml
+++ b/contrib/dp/dp_simplify.ml
@@ -10,8 +10,6 @@ let rec print_list sep print fmt = function
 let space fmt () = fprintf fmt "@ "
 
 let rec print_term fmt = function
-  | Tvar id -> 
-      fprintf fmt "%s" id
   | Cst n -> 
       fprintf fmt "%d" n
   | Plus (a, b) ->
@@ -70,8 +68,12 @@ let rec print_predicate fmt p =
 
 let print_query fmt (decls,concl) =
   let print_decl = function
-    | DeclVar _ | DeclPred _ | DeclType _ -> 
-	()
+    | DeclVar (id, _, _) ->
+	fprintf fmt "@[;; %s: <var>@]@\n" id
+    | DeclPred (id, _) -> 
+	fprintf fmt "@[;; %s: <predicate>@]@\n" id
+    | DeclType id ->
+	fprintf fmt "@[;; %s: TYPE@]@\n" id
     | Assert (id, f)  -> 
 	fprintf fmt "@[(BG_PUSH ;; %s@\n %a)@]@\n" id print_predicate f
   in
-- 
cgit v1.2.3