index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
cc
/
cctac.ml
Age
Commit message (
Expand
)
Author
2009-03-20
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2008-12-31
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
herbelin
2008-12-09
About "apply in":
herbelin
2008-11-09
f_equal : solve an inefficiency issue (apply vs. simple apply)
letouzey
2008-11-09
better fix for #1931 by using sort_of
letouzey
2008-09-14
Fix bug #1931 by searching for a sort after doing beta,iota,delta-
msozeau
2008-03-14
avoid universe problems with pf_get_type in f_equal
letouzey
2008-03-07
f_equal, revert, specialize in ML, contradict in better Ltac (+doc)
letouzey
2008-02-21
congruence now knows about _ -> _
corbinea
2007-10-18
added generation from trivial patterns for congruence
corbinea
2007-09-14
Correction du bug #1679 (congruence) et ajout test-suite
corbinea
2007-05-24
fixed (PR#1483)
corbinea
2007-03-15
Suppression argument pattern_source du case_info (code jamais utilisé)
herbelin
2006-09-19
added congruence improvement
corbinea
2006-01-21
Messages de idtac et fail peuvent maintenant être des listes de string, int ...
herbelin
2005-12-02
Changement des named_context
gregoire
2005-11-02
Types inductifs parametriques
mohring
2005-08-17
new congruence
corbinea
