aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-03-20 01:31:43 +0100
committerPierre-Marie Pédrot2016-03-20 01:57:19 +0100
commit0af598b77a6242d796c66884477a046448ef1e21 (patch)
treef0baff4fff51d0f6b785dafd01051aa37eb1c240 /kernel/nativecode.ml
parent8cb2040e4af40594826df97a735c38c8882934ca (diff)
Moving Tactic Notation to an EXTEND based command.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions