val auto_tac:
params:(NTacStatus.tactic_term list option * (string * string) list) ->
+ ?trace_ref:CicNotationPt.term list ref ->
's NTacStatus.tactic
+val keys_of_type:
+ (#NTacStatus.pstatus as 'a) ->
+ NTacStatus.cic_term -> 'a * NTacStatus.cic_term list
+