aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Correction trou de subject-reduction de create_arg dans genarg.mliGravatar herbelin2006-06-07
* Ajout WhelpGravatar herbelin2006-06-07
* petites corrections dans la doc de functional xxx. Gravatar courtieu2006-06-07
* Nouveaux Parametres InductifsGravatar cpaulin2006-06-07
* Réparation coqtop.mlGravatar notin2006-06-07
* Changement de l'option -where: on vérifie si la variable d'environnement COQ...Gravatar notin2006-06-07
* functional induction can now be used with Gravatar jforest2006-06-07
* mise en texttt d'une commande.Gravatar courtieu2006-06-07
* Changements sur Functional xxx. Plus précis et plus exact.Gravatar courtieu2006-06-07
* Ajout de précisions dans la doc de functional scheme et consort +Gravatar courtieu2006-06-06
* this time it's good Gravatar jforest2006-06-06
* Error in last commit Gravatar jforest2006-06-06
* Debut modif parametres inductifs CICGravatar cpaulin2006-06-06
* protecting an uncaught exception Not_found Gravatar jforest2006-06-06
* reparation pour le bug #1072 (soufflee par J. Forest): Gravatar letouzey2006-06-06
* + ameliorating the tactic "functional induction"Gravatar jforest2006-06-06
* Oh le joli bug dans le kernel:Gravatar letouzey2006-06-05
* Require FSets ne doit pas charger FSetToFiniteSet (qui utilise l'axiome d'ext...Gravatar letouzey2006-06-05
* nouveaux parametresGravatar cpaulin2006-06-05
* MAJ svn:ignore coqc.opt et coqmktop.optGravatar herbelin2006-06-04
* Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict wit...Gravatar herbelin2006-06-04
* Ajout exists! et restructuration/extension des fichiers sur laGravatar herbelin2006-06-04
* Ajout exists! et restructuration/extension des fichiers sur laGravatar herbelin2006-06-04
* debut de reparation du test d'extractionGravatar letouzey2006-06-02
* Update Program/subtac documentation.Gravatar msozeau2006-06-01
* Fix some nasty bug with the evars-to-dependent sum encoding.Gravatar msozeau2006-06-01
* bug in alpha-conversionGravatar jforest2006-06-01
* reparation bug #1128Gravatar letouzey2006-06-01
* Fusion if.v et If.v (MacOS X ne sait pas distinguer la casse)Gravatar herbelin2006-05-31
* Fusion destruct.v et Destruct.v (MacOS X ne sait pas distinguer la casseGravatar herbelin2006-05-31
* ajout de QArith dans les theories standardsGravatar letouzey2006-05-31
* petits ajoutsGravatar letouzey2006-05-31
* Replacing the old version of "functional induction" with the new one. Gravatar jforest2006-05-31
* Colorisation dans CoqideGravatar notin2006-05-31
* retour au comportement antérieur pour une application de foncteur: Gravatar letouzey2006-05-30
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Correction bug #990 (LoadPath et option -R de coqideGravatar notin2006-05-30
* * suite de la revision des wrappers MakeGravatar letouzey2006-05-30
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
* Fix broken paths.Gravatar msozeau2006-05-29
* small changes Gravatar jforest2006-05-29
* Ajout d'alias pour prodT_rect et cie qui avaient été oublkÃiésGravatar herbelin2006-05-29
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
* Adaptation au passage de sig2 dans TypeGravatar herbelin2006-05-28
* Adaptation au passage de vector dans TypeGravatar herbelin2006-05-28
* Adaptation au passage de option dans TypeGravatar herbelin2006-05-28
* Ajout array_fold_map2Ã'Gravatar herbelin2006-05-28
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
* Modification de la compilation de coqc et coqmktop pour éviter le problème ...Gravatar notin2006-05-26
* Added contrib/funind to the path for ocamldebug-coqGravatar courtieu2006-05-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 20:57:13 +0000