diff options
| author | coq | 2005-04-21 14:34:19 +0000 |
|---|---|---|
| committer | coq | 2005-04-21 14:34:19 +0000 |
| commit | f454cc6dff2eadd720c126b8b43dff032efdb129 (patch) | |
| tree | 6328b968a387d43a89a956a492fc6c1c2e924752 /contrib/dp/dp_simplify.ml | |
| parent | a72689957c58ebe5d428c40b2b9387cc9cdf95a3 (diff) | |
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
Diffstat (limited to 'contrib/dp/dp_simplify.ml')
| -rw-r--r-- | contrib/dp/dp_simplify.ml | 10 |
1 files changed, 6 insertions, 4 deletions
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 |