diff options
| author | mohring | 2002-01-31 13:07:40 +0000 |
|---|---|---|
| committer | mohring | 2002-01-31 13:07:40 +0000 |
| commit | d3ca56683d0977ed4cb7acc0d61c5d83ecc939c1 (patch) | |
| tree | afb628657007ff33cdc2db21e769da76fe6c3d19 /tactics | |
| parent | 4fef76aefe06938fc724e66c08ff51b501cf0dfa (diff) | |
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
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 |