index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
Commit message (
Expand
)
Author
Age
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Suite commit 11236
notin
2008-07-24
*
Stop glob messages to be printed by default on stdout
letouzey
2008-07-23
*
Correct implementation of discharging of implicit arguments and add new
msozeau
2008-07-22
*
Oubli lors du commit #11236
notin
2008-07-22
*
Suite commit 11236
notin
2008-07-21
*
Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...
notin
2008-07-18
*
Modification rapide du message d'erreur lorsqu'un _ ne peut être
herbelin
2008-07-18
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
Autour du parsing:
herbelin
2008-07-15
*
Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...
notin
2008-07-07
*
- Improve [Context] vernacular to allow arbitrary binders, not just
msozeau
2008-07-07
*
Fixes in handling of implicit arguments:
msozeau
2008-07-04
*
Documentation Prop<=Set et Arguments Scope Global
herbelin
2008-07-01
*
Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...
notin
2008-06-25
*
Code cleanup in typeclasses, remove dead and duplicated code.
msozeau
2008-06-21
*
Correction bug 1878 (utilisation de extend_evar déplacée là où une
herbelin
2008-06-14
*
- Extension de "generalize" en "generalize c as id at occs".
herbelin
2008-06-08
*
Enhancements to coqdoc, better globalization of sections and modules.
msozeau
2008-06-06
*
Fix setoid_rewrite documentation examples.
msozeau
2008-06-03
*
Improvements on coqdoc by adding more information into .glob
msozeau
2008-05-30
*
Notation concise pour la valeur par défaut des cas reconnus comme
herbelin
2008-05-28
*
Ajout de la possibilité d'utiliser fix/cofix dans les notations.
herbelin
2008-05-24
*
Fix "not an applied typeclass" error for legitimate classes
msozeau
2008-05-12
*
- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait des
herbelin
2008-05-10
*
Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757
herbelin
2008-05-07
*
Better parsing of typeclasses, any constr is allowed for ! bindings so
msozeau
2008-05-06
*
Postpone the search for the recursive argument index from the user given
msozeau
2008-05-06
*
Factorize code for internalization of binders to fix bug #1846. Also
msozeau
2008-05-04
*
Diverses corrections
herbelin
2008-04-14
*
Bugs, nettoyage, et améliorations diverses
herbelin
2008-04-13
*
Add the ability to specify what to do with free variables in instance
msozeau
2008-04-12
*
Correction bug List.map2 dans Case12.v
herbelin
2008-04-09
*
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
*
Enhance handling of parameters in typeclass constraints: permit to specify an...
msozeau
2008-04-01
*
- Fix for rewriting under dependent products.
msozeau
2008-03-31
*
Modifications diverses et variées :
herbelin
2008-03-30
*
Ajout d'abbréviations/notations paramétriques
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
*
Finish fix in command where we still lost information on what was a type
msozeau
2008-03-24
*
Fix a bug found by B. Grégoire when declaring morphisms in module
msozeau
2008-03-23
*
Add a flag to control rewriting under lambdas. Otherwise makes some
msozeau
2008-03-20
*
Do another pass on the typeclasses code. Correct globalization of class
msozeau
2008-03-19
*
Do a second pass on the treatment of user-given implicit arguments. Now
msozeau
2008-03-15
*
Move generally useful definition of nf_evar on contexts to evarutil.
msozeau
2008-02-08
*
Beaoucoup de changements dans la representation interne des modules.
soubiran
2008-02-01
*
Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...
msozeau
2008-01-17
[next]