]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/proofEngine.ml
projects / helm.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
First commit of our future proof-assistant/proof-improver (???)
[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;;
Unnamed repository; edit this file 'description' to name the repository.