index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
Commit message (
Expand
)
Author
Age
*
Prise en compte des coercions dans les clauses "with" même si le type
herbelin
2008-04-23
*
Test que la bibliothèque ZArith est chargée lors d'un appel à simplify, er...
notin
2008-04-22
*
- Parameterize unification by two sets of transparent_state, one for open
msozeau
2008-04-21
*
Addded the "Dump Tree" command.
cek
2008-04-21
*
tactique gappa
filliatr
2008-04-17
*
Little fixes in setoid_rewrite.
msozeau
2008-04-17
*
first-order --> firstorder (kills a warning about not being a valid id)
letouzey
2008-04-16
*
flottants
filliatr
2008-04-16
*
- Add "Global" modifier for instances inside sections with the usual
msozeau
2008-04-15
*
fix some bogus calls to id_of_string by the extraction
letouzey
2008-04-15
*
oubli sur 10790
herbelin
2008-04-14
*
Diverses corrections
herbelin
2008-04-14
*
Bugs, nettoyage, et améliorations diverses
herbelin
2008-04-13
*
Désactivation du dumping des notations quand funind appelle les
herbelin
2008-04-12
*
Add the ability to specify what to do with free variables in instance
msozeau
2008-04-12
*
Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.
msozeau
2008-04-12
*
Check that no evars remain in instance types earlier at Instance
msozeau
2008-04-11
*
Verify Setoid is loaded only if we're not in Coq.Classes.*. Add explicit
msozeau
2008-04-09
*
correction of bug 1829
jforest
2008-04-08
*
- A little cleanup in Classes/*. Separate standard morphisms on
msozeau
2008-04-08
*
Fix big de Bruijn bug in mutually recursive definitions.
msozeau
2008-04-07
*
Correction problème de compil (blast.ml)
herbelin
2008-04-04
*
Quelques améliorations des intro patterns:
herbelin
2008-04-04
*
Add the ability to specify the implicit status of section variables and
msozeau
2008-04-02
*
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient
herbelin
2008-04-01
*
Ajout "simple apply" et "simple eapply" pour apply sans unfold
herbelin
2008-04-01
*
Add option to set the opacity of obligations to transparent, to be able
msozeau
2008-04-01
*
Suite commit 10730: MAJ xlate.ml
herbelin
2008-03-30
*
- Second pass on implementation of let pattern. Parse "let ' par [as x]?
msozeau
2008-03-28
*
Various fixes on typeclasses:
msozeau
2008-03-27
*
Fix a bug found by B. Grégoire when declaring morphisms in module
msozeau
2008-03-23
*
Une passe sur les réels:
herbelin
2008-03-23
*
Do another pass on the typeclasses code. Correct globalization of class
msozeau
2008-03-19
*
tactique gappa
filliatr
2008-03-19
*
Added a function to rebuild an elim scheme from elim_scheme_info. Will
courtieu
2008-03-18
*
Removed unneeded tactics from RelationClasses. Use
msozeau
2008-03-16
*
Reorganize Program and Classes theories. Requiring Setoid no longer sets
msozeau
2008-03-16
*
Minor fixes on setoid rewriting. Now uses definitions of [relation] and
msozeau
2008-03-16
*
Do a second pass on the treatment of user-given implicit arguments. Now
msozeau
2008-03-15
*
Adapt funind to the RLetPattern constructor.
msozeau
2008-03-15
*
avoid universe problems with pf_get_type in f_equal
letouzey
2008-03-14
*
Backtrack wrong commit.
courtieu
2008-03-14
*
kill a warning (and clean the code around)
letouzey
2008-03-14
*
nettoyage de code obsolete.
soubiran
2008-03-14
*
Ajout des alias de module dans le noyau.
soubiran
2008-03-14
*
tactique gappa
filliatr
2008-03-14
*
indentation.
courtieu
2008-03-14
*
trying f
courtieu
2008-03-13
*
tactique Gappa : mise en place
filliatr
2008-03-11
*
Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)
herbelin
2008-03-10
[next]