index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
context.ml
Age
Commit message (
Expand
)
Author
2016-02-09
REFORMATTING: kernel/context.ml{,i}
Matej Kosik
2016-02-09
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-11
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2015-12-05
Moving extended_rel_vect/extended_rel_list to the kernel.
Hugo Herbelin
2015-01-12
Update headers.
Maxime Dénès
2014-10-24
Remove an ununsed pattern and commented code in the kernel.
Matthieu Sozeau
2014-10-22
Pushing Pierre's factorization of names in goal context printing from
Hugo Herbelin
2014-10-20
A patch for printing "match" when constructors are defined with let-in
Hugo Herbelin
2014-09-01
Coqide prints succesive hyps of the same type on 1 line
Pierre Boutillier
2013-10-22
Removing some generic equalities.
ppedrot
2013-08-04
Removing useless casts between arrays and lists.
ppedrot
2013-04-29
Merging Context and Sign.
ppedrot
2013-04-29
Splitting Term into five unrelated interfaces:
ppedrot
