diff options
| author | Pierre-Marie Pédrot | 2016-04-28 09:47:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-02 08:02:35 +0200 |
| commit | 54277abbf0fa15e0437d2a68859ceeef09ec70c3 (patch) | |
| tree | 56e5f02ea49973480a9e1570f74011ac06809844 | |
| parent | c5b6321df0f83d6b29489bbddb920bdb1ebb96a8 (diff) | |
Useless code in Tacentries.
| -rw-r--r-- | ltac/tacentries.ml | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index f94f84a73b..0be0dc7dcd 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -149,20 +149,15 @@ let add_tactic_entry (kn, ml, tg) = let open Tacexpr in let entry, pos = get_tactic_entry tg.tacgram_level in let mkact loc l = - let filter = function - | GramTerminal _ -> None - | GramNonTerminal (_, t, _) -> Some (Genarg.unquote t) - in - let types = List.map_filter filter tg.tacgram_prods in - let map arg t = + let map arg = (** HACK to handle especially the tactic(...) entry *) let wit = Genarg.rawwit Constrarg.wit_tactic in - if Genarg.argument_type_eq t (Genarg.unquote wit) && not ml then + if Genarg.has_type arg wit && not ml then Tacexp (Genarg.out_gen wit arg) else TacGeneric arg in - let l = List.map2 map l types in + let l = List.map map l in (TacAlias (loc,kn,l):raw_tactic_expr) in let () = |