Default tactic for solving goals.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9460 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 16 insertions, 11 deletions

diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index fda13a12e1..c144f1f9eb 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -120,6 +120,8 @@ let subtac_end_proof = function
 open Pp
 open Ppconstr
 open Decl_kinds
+open Tacinterp
+open Tacexpr
 
 let start_proof_com env isevars sopt kind (bl,t) hook =
   let id = match sopt with
@@ -140,6 +142,14 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
       
 let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
 
+let subtac_utils_path =
+  make_dirpath (List.map id_of_string ["Utils";contrib_name;"Coq"])
+let utils_tac s =
+  lazy(make_kn (MPfile subtac_utils_path) (make_dirpath []) (mk_label s))
+
+let utils_call tac args =
+  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (utils_tac tac)),args))
+
 let start_proof_and_print env isevars idopt k t hook =
   start_proof_com env isevars idopt k t hook;
   print_subgoals ()
@@ -148,10 +158,11 @@ let start_proof_and_print env isevars idopt k t hook =
 let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
-  check_required_library ["Coq";"Logic";"JMeq"];  
+  check_required_library ["Coq";"Logic";"JMeq"];
   require_library "Coq.subtac.FixSub";
   require_library "Coq.subtac.Utils";
-  (*Subtac_obligations.set_default_tactic (Tacinterp.lookup_tactic "subtac_simpl" []);*)
+  Subtac_obligations.set_default_tactic 
+    (Tacinterp.eval_tactic (utils_call "subtac_simpl" []));
   let env = Global.env () in
   let isevars = ref (create_evar_defs Evd.empty) in
   try
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index d49ff7e21c..7096d439ee 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1625,7 +1625,7 @@ let constr_of_pat env isevars ty pat =
 	    ([], [], env, 0) ci.cs_args (List.rev args)
 	in
 	let cstr = mkConstruct ci.cs_cstr in
-	let app = applistc cstr params in
+	let app = applistc cstr (List.map (lift (List.length args)) params) in
 	let app = applistc app (List.rev args) in
 	  if alias <> Anonymous then
 	    (alias, Some app, ty) :: sign, lift 1 app, n + 1
diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v
index 07f63a2ba8..f73507d2f5 100644
--- a/contrib/subtac/test/take.v
+++ b/contrib/subtac/test/take.v
@@ -1,14 +1,13 @@
-Variable A : Set.
 Require Import JMeq.
 Require Import List.
 Require Import Coq.subtac.Utils.
 
-Program Fixpoint take (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
+Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
   match n with
   | 0 => nil
   | S p => 
     match l with
-    | cons hd tl => let rest := take tl p in cons hd rest
+    | cons hd tl => let rest := take A tl p in cons hd rest
     | nil => _
     end
   end.
@@ -22,18 +21,13 @@ Solve Obligations using (subtac_simpl ; subst ; auto with arith).
 Obligations.
 
 Obligation 3.
-  subtac_simpl.
   destruct_call take ; subtac_simpl ; subst ; auto.
 Defined.
 
 Obligation 4.
-  subtac_simpl.
   subst l x.
   simpl in l0.
   absurd (S p <= 0) ; omega.
 Defined.
 
-
-Print take.
-
 Extraction take.