From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 contrib/first-order/g_ground.ml4 | 41 +++++++++++++++++++++++++++++++++++-----
 1 file changed, 36 insertions(+), 5 deletions(-)

(limited to 'contrib/first-order/g_ground.ml4')

diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index f9c4cea2..366f563b 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma"  i*)
 
-(* $Id: g_ground.ml4 8752 2006-04-27 19:37:33Z herbelin $ *)
+(* $Id: g_ground.ml4 9154 2006-09-20 17:18:18Z corbinea $ *)
 
 open Formula
 open Sequent
@@ -24,7 +24,7 @@ open Libnames
 
 (* declaring search depth as a global option *)
 
-let ground_depth=ref 5
+let ground_depth=ref 3
 
 let _=
   let gdopt=
@@ -34,13 +34,28 @@ let _=
       optread=(fun ()->Some !ground_depth); 
       optwrite=
    (function 
-	None->ground_depth:=5
+	None->ground_depth:=3
       |	Some i->ground_depth:=(max i 0))}
   in
     declare_int_option gdopt
-      
+
+let congruence_depth=ref 100
+
+let _=
+  let gdopt=
+    { optsync=true;
+      optname="Congruence Depth";
+      optkey=SecondaryTable("Congruence","Depth"); 
+      optread=(fun ()->Some !congruence_depth); 
+      optwrite=
+   (function 
+	None->congruence_depth:=0
+      |	Some i->congruence_depth:=(max i 0))}
+  in
+    declare_int_option gdopt
+
 let default_solver=(Tacinterp.interp <:tactic<auto with *>>)
-    
+
 let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
 		      
 type external_env=
@@ -94,3 +109,19 @@ TACTIC EXTEND gintuition
   [ "gintuition" tactic_opt(t) ] ->
      [ gen_ground_tac false (option_map eval_tactic t) Void ]
 END
+
+
+let default_declarative_automation gls = 
+  tclORELSE 
+    (Cctac.congruence_tac !congruence_depth []) 
+    (gen_ground_tac true 
+       (Some (tclTHEN
+		default_solver
+		(Cctac.congruence_tac !congruence_depth [])))
+       Void) gls
+
+
+
+let () = 
+  Decl_proof_instr.register_automation_tac default_declarative_automation
+
-- 
cgit v1.2.3