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
*
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
*
Fix compilation problem and finish little cleanup.
msozeau
2008-03-10
*
Fix a few bugs in Program: use user-given typing constraints for
msozeau
2008-03-09
*
correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)
jforest
2008-03-08
*
f_equal, revert, specialize in ML, contradict in better Ltac (+doc)
letouzey
2008-03-07
*
Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part
msozeau
2008-03-07
*
Plug the new setoid implemtation in, leaving the original one commented
msozeau
2008-03-06
*
Syntax changes in typeclasses, remove "?" for usual implicit arguments
msozeau
2008-03-06
*
Attempt of fix for extraction of modules types
letouzey
2008-03-05
*
Rework on rich forms of rewrite
letouzey
2008-03-01
*
dead code
letouzey
2008-02-27
*
typo
letouzey
2008-02-27
*
Proper implicit arguments handling for assumptions
msozeau
2008-02-26
*
Forgotten file in previous commit
lmamane
2008-02-25
*
Merge with lmamane's private branch:
lmamane
2008-02-22
*
congruence now knows about _ -> _
corbinea
2008-02-21
*
Petite correction suite à la révision 10571
notin
2008-02-18
*
Backport Program Instance into Instance. Proper early error message if
msozeau
2008-02-10
*
Solde de code mort et petites optimisations sur lesquels je suis
herbelin
2008-02-09
*
Change implementation of resolution for typeclasses to use a customized
msozeau
2008-02-08
*
New "Preterm [ of id ] " command to show the preterm before giving it to
msozeau
2008-02-08
*
Backport code from command.ml to subtac_command.ml for definining
msozeau
2008-02-08
*
New algorithm to resolve morphisms, after discussion with Nicolas
msozeau
2008-02-06
*
Beaoucoup de changements dans la representation interne des modules.
soubiran
2008-02-01
[next]