diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 19 | ||||
| -rw-r--r-- | tactics/tactics.mli | 1 |
2 files changed, 19 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5e72ed2dd8..ef430f9b64 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 [] diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 734895730c..2df23a30fb 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -231,6 +231,7 @@ val constructor_checking_bound : int option -> int -> constr substitution -> tactic val one_constructor : int -> constr substitution -> tactic val any_constructor : tactic +val tclConstrThen : tactic -> tactic val left : constr substitution -> tactic val simplest_left : tactic val right : constr substitution -> tactic |