From 9cb6bb1624719baa6d0d05f89bc8a537b4111b69 Mon Sep 17 00:00:00 2001
From: coq
Date: Wed, 16 Mar 2005 10:18:21 +0000
Subject: tactiques prouveurs premier ordre dans contrib/dp/

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

(limited to 'contrib')

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index b60a27e631..529a105097 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -5,9 +5,14 @@ open Term
 open Tacmach
 open Fol
 
-let simplify gl =
+type prover = Simplify | CVCLite | Harvey
+
+let dp prover gl =
   let concl = pf_concl gl in
   if not (is_Prop (pf_type_of gl concl)) then error "not a proposition";
-  msgnl (str "nb of hyps = " ++ int (List.length (pf_hyps gl)));
-  pp_flush ();
   error "not yet implemented"
+
+let simplify = dp Simplify
+let cvc_lite = dp CVCLite
+let harvey = dp Harvey
+
-- 
cgit v1.2.3