]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/proofEngine.ml
fc0df2d02e50521ed730a0d25e9fe295f7069486
[helm.git] / helm / gTopLevel / proofEngine.ml
1 type binder_type =
2    Declaration
3  | Definition
4 ;;
5
6 type context = (binder_type * Cic.name * Cic.term) list;;
7
8 type sequent = context * Cic.term;;