changement generation de schema d'elimination, False_rec est primitif, Constructor tac

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

1 files changed, 18 insertions, 1 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5e72ed2dd..ef430f9b6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -995,12 +995,29 @@ let any_constructor gl =
   tclFIRST (List.map (fun i -> one_constructor i []) 
               (interval 1 nconstr)) gl
 
+(* Try to apply the constructor of the inductive definition followed by 
+   a tactic t given as an argument.
+   Should be generalize in Constructor (Fun c : I -> tactic)
+ *)
+
+let tclConstrThen t gl = 
+  let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl))
+  in let lconstr =
+       (snd (Global.lookup_inductive mind)).mind_consnames
+  in let nconstr = Array.length lconstr 
+  in
+  if nconstr = 0 then error "The type has no constructors";
+  tclFIRST (List.map (fun i -> (tclTHEN (one_constructor i []) t))
+              (interval 1 nconstr)) gl
+
 let dyn_constructor = function 
   | [Integer i; Bindings binds]  -> tactic_bind_list (one_constructor i) binds
   | [Integer i; Cbindings binds] -> (one_constructor i) binds
+  | [Tac (tac,_)] -> tclConstrThen tac
   | []                           -> any_constructor 
   | l                            -> bad_tactic_args "constructor" l
-                       
+
+
 let left           = (constructor_checking_bound (Some 2) 1)
 let simplest_left  = left  []