diff options
author | 2008-04-04 16:25:05 +0000 | |
---|---|---|
committer | 2008-04-04 16:25:05 +0000 | |
commit | bc8728f0762f7e39f779c677679a8bc351a4290a (patch) | |
tree | b8a131508fcd4bc0ca131d4032788316b08b6997 /tactics | |
parent | 2814afbbd4803216ad4cb6af9ec5d86fce71e8eb (diff) |
- Relâchement de la contrainte de bonne longueur des intropatterns
lorsqu'en position terminale (en fait, l'idéal serait de pouvoir
mettre des tactiques dans les branches, style "intros [H ; tac | ]")
(cf un exemple QvMake.v)
- Pas de delta du tout quand on fait de la recherche de sous-terme
(même lorsqu'on vient de apply avec une conclusion ?P t) (cf un
exemple dans Rocq/DEMOS/Sorting.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10755 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/tactics.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3a2ec3705..ac72c4479 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -984,17 +984,18 @@ let intro_or_and_pattern ll l' tac = tclLAST_HYP (fun c gl -> let ind,_ = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in let nv = mis_constr_nargs ind in - let rec adjust_names_length force n = function - | [] when n = 0 or not force -> [] - | [] -> IntroAnonymous :: adjust_names_length force (n-1) [] - | _ :: _ when n = 0 -> error "Too many names in some branch" - | ip :: l -> ip :: adjust_names_length force (n-1) l in + let rec adjust_names_length tail n = function + | [] when n = 0 or tail -> [] + | [] -> IntroAnonymous :: adjust_names_length tail (n-1) [] + | _ :: _ as l when n = 0 -> + if tail then l else error "Too many names in some branch" + | ip :: l -> ip :: adjust_names_length tail (n-1) l in let ll = fix_empty_case nv ll in if List.length ll <> Array.length nv then error "Not the right number of patterns"; tclTHENLASTn (tclTHEN case_last clear_last) - (array_map2 (fun n l -> tac ((adjust_names_length (l'<>[]) n l)@l')) + (array_map2 (fun n l -> tac ((adjust_names_length (l'=[]) n l)@l')) nv (Array.of_list ll)) gl) |