index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
toplevel
/
auto_ind_decl.ml
Age
Commit message (
Expand
)
Author
2009-12-12
Updated compatibility for rewriting equality proofs that are dependent
herbelin
2009-11-08
Fixed "Scheme Equality" when another instance of the scheme on the
herbelin
2009-11-08
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-10-21
This big commit addresses two problems:
soubiran
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-08-04
- Add more precise error localisation when one of the application fails
herbelin
2009-03-16
Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"
herbelin
2008-12-09
About "apply in":
herbelin
2008-10-26
Fixes and refinements regarding occurrence selection:
herbelin
2008-08-04
Évolutions diverses et variées.
herbelin
2008-06-21
- Implantation de la suggestion 1873 sur discriminate. Au final,
herbelin
2008-06-10
- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)
herbelin
2008-06-08
- Extension de "generalize" en "generalize c as id at occs".
herbelin
2008-04-12
Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.
msozeau
2008-04-01
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient
herbelin
2008-03-17
* Factorizing code : context_chop was used in several files (even as chop_con...
vsiles
2007-12-18
Nettoyage de code en vue de la release. Plus de Warning: Unused
aspiwack
2007-12-06
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-10-05
Added the automatic generation of the boolean equality if possible and the
vsiles
