1 files changed, 103 insertions, 0 deletions
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
new file mode 100644
index 00000000..f85f2171
--- /dev/null
+++ b/contrib/first-order/g_ground.ml4
@@ -0,0 +1,103 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma"  i*)
+
+(* $Id: g_ground.ml4,v 1.10.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+
+open Formula
+open Sequent
+open Ground
+open Goptions
+open Tactics
+open Tacticals
+open Tacinterp
+open Term
+open Names
+open Util
+open Libnames
+
+(* declaring search depth as a global option *)
+
+let ground_depth=ref 5
+
+let _=
+  let gdopt=
+    { optsync=true;
+      optname="Firstorder Depth";
+      optkey=SecondaryTable("Firstorder","Depth"); 
+      optread=(fun ()->Some !ground_depth); 
+      optwrite=
+   (function 
+	None->ground_depth:=5
+      |	Some i->ground_depth:=(max i 0))}
+  in
+    declare_int_option gdopt
+      
+let default_solver=(Tacinterp.interp <:tactic<auto with *>>)
+    
+let fail_solver=tclFAIL 0 "GTauto failed"
+		      
+type external_env=
+    Ids of global_reference list
+  | Bases of Auto.hint_db_name list
+  | Void
+
+let gen_ground_tac flag taco ext gl=
+  let backup= !qflag in
+    try
+      qflag:=flag;
+      let solver= 
+	match taco with 
+	    Some tac-> tac
+	  | None-> default_solver in
+      let startseq=
+	match ext with
+	    Void -> (fun gl -> empty_seq !ground_depth)
+	  | Ids l-> create_with_ref_list l !ground_depth
+	  | Bases l-> create_with_auto_hints l !ground_depth in
+      let result=ground_tac solver startseq gl in 
+	qflag:=backup;result
+    with e ->qflag:=backup;raise e
+      
+(* special for compatibility with Intuition 
+
+let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
+
+let defined_connectives=lazy
+  [[],EvalConstRef (destConst (constant "not"));
+   [],EvalConstRef (destConst (constant "iff"))]
+
+let normalize_evaluables=
+  onAllClauses
+    (function 
+	 None->unfold_in_concl (Lazy.force defined_connectives)
+       | Some id-> 
+	   unfold_in_hyp (Lazy.force defined_connectives) 
+	   (Tacexpr.InHypType id)) *)
+
+TACTIC EXTEND Firstorder
+    [ "Firstorder" tactic_opt(t) "with" ne_reference_list(l) ] -> 
+      [ gen_ground_tac true (option_app eval_tactic t) (Ids l) ]
+|   [ "Firstorder" tactic_opt(t) "using" ne_preident_list(l) ] -> 
+      [ gen_ground_tac true (option_app eval_tactic t) (Bases l) ]
+|   [ "Firstorder" tactic_opt(t) ] -> 
+      [ gen_ground_tac true (option_app eval_tactic t) Void ]
+END
+
+(* Obsolete since V8.0
+TACTIC EXTEND GTauto   
+  [ "GTauto" ] ->
+     [ gen_ground_tac false (Some fail_solver) Void ]   
+END
+*)
+
+TACTIC EXTEND GIntuition
+  [ "GIntuition" tactic_opt(t) ] ->
+     [ gen_ground_tac false (option_app eval_tactic t) Void ]
+END