aboutsummaryrefslogtreecommitdiff
path: root/dev/inc_ltac
blob: 8ef02445c24a4fefc7c8c7a61da7382c539c33fa (plain)
1
2
3
4
5
6
7
open Evar_tactics
open Tactic_debug
open Tacsubst
open Tacintern
open Tacinterp
open Extraargs
open Extratactics