diff options
| author | Hugo Herbelin | 2014-09-24 14:36:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-24 15:04:30 +0200 |
| commit | e24a118644d77e86ace11a34230711b204025c3b (patch) | |
| tree | a5762a0628cb3fbb515046fb177937d8a36add38 | |
| parent | 507732b8541dea205e4e0288f81ea0eb58a7c253 (diff) | |
Added support for interpreting hyp lists in tactic notations.
| -rw-r--r-- | tactics/tacinterp.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index ab2dbe6ffe..65794a0c0e 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -385,8 +385,18 @@ let interp_occurrences ist occs = let interp_hyp_location ist env sigma ((occs,id),hl) = ((interp_occurrences ist occs,interp_hyp ist env sigma id),hl) +let interp_hyp_location_list_as_list ist env sigma ((occs,id),hl as x) = + match occs,hl with + | AllOccurrences,InHyp -> + List.map (fun id -> ((AllOccurrences,id),InHyp)) + (interp_hyp_list_as_list ist env sigma id) + | _,_ -> [interp_hyp_location ist env sigma x] + +let interp_hyp_location_list ist env sigma l = + List.flatten (List.map (interp_hyp_location_list_as_list ist env sigma) l) + let interp_clause ist env sigma { onhyps=ol; concl_occs=occs } : clause = - { onhyps=Option.map(List.map (interp_hyp_location ist env sigma)) ol; + { onhyps=Option.map (interp_hyp_location_list ist env sigma) ol; concl_occs=interp_occurrences ist occs } (* Interpretation of constructions *) |