diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-03-24 15:03:21 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-03-24 15:03:21 +0000 |
| commit | bf7592d6ea7bd0e485d02c45f25c29b82c2d43c5 (patch) | |
| tree | a24374927e2f170add787aee0ee7fa0d451f89e8 /contrib/dp/dp_simplify.ml | |
| parent | f29563be843fd72adb742a2f03404ea3e13e4825 (diff) | |
symboles de fonctions globaux traites
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6882 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/dp/dp_simplify.ml')
| -rw-r--r-- | contrib/dp/dp_simplify.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml index 35370c6fd..353bb7092 100644 --- a/contrib/dp/dp_simplify.ml +++ b/contrib/dp/dp_simplify.ml @@ -76,7 +76,7 @@ let rec print_predicate fmt p = let print_query fmt (decls,concl) = let print_decl = function - | DeclVar _ | DeclProp _ | DeclType _ -> + | DeclVar _ | DeclPred _ | DeclType _ -> () | Assert (id, f) -> fprintf fmt "@[(BG_PUSH ;; %s@\n %a)@]@\n" id print_predicate f |