diff options
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 40 |
1 files changed, 17 insertions, 23 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 6f6c4a05a..14e0fed31 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -718,35 +718,29 @@ and intern_match_rule onlytac ist = function Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl) | [] -> [] -and intern_genarg ist x = - match genarg_tag x with - | ListArgType _ -> - let list_unpacker wit l = - let map x = - let ans = intern_genarg ist (in_gen (rawwit wit) x) in - out_gen (glbwit wit) ans - in - in_gen (glbwit (wit_list wit)) (List.map map (raw l)) +and intern_genarg ist (GenArg (Rawwit wit, x)) = + match wit with + | ListArg wit -> + let map x = + let ans = intern_genarg ist (in_gen (rawwit wit) x) in + out_gen (glbwit wit) ans in - list_unpack { list_unpacker } x - | OptArgType _ -> - let opt_unpacker wit o = match raw o with + in_gen (glbwit (wit_list wit)) (List.map map x) + | OptArg wit -> + let ans = match x with | None -> in_gen (glbwit (wit_opt wit)) None | Some x -> let s = out_gen (glbwit wit) (intern_genarg ist (in_gen (rawwit wit) x)) in in_gen (glbwit (wit_opt wit)) (Some s) in - opt_unpack { opt_unpacker } x - | PairArgType _ -> - let pair_unpacker wit1 wit2 o = - let p, q = raw o in - let p = out_gen (glbwit wit1) (intern_genarg ist (in_gen (rawwit wit1) p)) in - let q = out_gen (glbwit wit2) (intern_genarg ist (in_gen (rawwit wit2) q)) in - in_gen (glbwit (wit_pair wit1 wit2)) (p, q) - in - pair_unpack { pair_unpacker } x - | ExtraArgType s -> - snd (Genintern.generic_intern ist x) + ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = out_gen (glbwit wit1) (intern_genarg ist (in_gen (rawwit wit1) p)) in + let q = out_gen (glbwit wit2) (intern_genarg ist (in_gen (rawwit wit2) q)) in + in_gen (glbwit (wit_pair wit1 wit2)) (p, q) + | ExtraArg s -> + snd (Genintern.generic_intern ist (in_gen (rawwit wit) x)) (** Other entry points *) |