aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Modification of emacs output: Pp.warning and al now output warningGravatar courtieu2006-04-27
* préparation de add_glob en vue d'isolement de la partie module pourGravatar herbelin2006-04-27
* Ajout chop_dirpathGravatar herbelin2006-04-27
* 2-3 lemmes en plus pour que les Bvectors soient effectivement utilisablesGravatar letouzey2006-04-27
* Added a short doc for "Function". To be finished.Gravatar courtieu2006-04-27
* MAJGravatar herbelin2006-04-26
* - Utilisation d'abbréviations pour les types intervenant dans RCasesGravatar herbelin2006-04-26
* Outil de test de la réversibilité du réafficheur v8->v8Gravatar herbelin2006-04-26
* Diverses corrections de l'afficheur et du traducteur pour s'assurer deGravatar herbelin2006-04-26
* Régénération après mise à jour coqdep pour traiter Require multipleGravatar herbelin2006-04-26
* Prise en compte du Require multipleGravatar herbelin2006-04-26
* suite du pont entre Bvector et NGravatar letouzey2006-04-26
* Replacing "GenFixpoint" with "Function" and "mes" with "measure"Gravatar jforest2006-04-26
* Correction d'un bug dans coqdoc sur l'utilisation de l'option -o et la créat...Gravatar notin2006-04-26
* Un gros coup de lifting pour IntMap: Gravatar letouzey2006-04-25
* un lemme de double inclusionGravatar letouzey2006-04-25
* Reverting nf_betaiotaevar_preserving_vm_castGravatar jforest2006-04-25
* Code mort (suite)Gravatar herbelin2006-04-25
* Suppression code mortGravatar herbelin2006-04-25
* Timide tentative de clarification du statut de l'opérateur de filtrageGravatar herbelin2006-04-24
* Changement anomaly en failwith dans out_name pour utilisation par map_succeedGravatar herbelin2006-04-24
* Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr;Gravatar herbelin2006-04-24
* + Handling "if" and cast in GenFixpoint Gravatar jforest2006-04-24
* decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)Gravatar letouzey2006-04-20
* Nouveau mécanisme pour les modules interactifs : les arguments deGravatar herbelin2006-04-16
* Added code to support "Program Lemma/Example... etc"Gravatar msozeau2006-04-16
* Inversion de l'ordre de chargement des objets logiques et non logiquesGravatar herbelin2006-04-15
* Tests notationsGravatar herbelin2006-04-15
* Test synchronisation chargement objets non logiquesGravatar herbelin2006-04-15
* Si un fixpoint a plusieurs arguments, mais un seul de type inductif, Gravatar letouzey2006-04-14
* Pas fierGravatar herbelin2006-04-14
* mise a jour creditsGravatar cpaulin2006-04-14
* Enleve les commentairesGravatar cpaulin2006-04-14
* Test files for subtac.Gravatar msozeau2006-04-14
* Maj configure, README, etc...Gravatar notin2006-04-14
* Premier jet annonce 8.1Gravatar herbelin2006-04-14
* MAJ 8.1Gravatar herbelin2006-04-14
* replacing whd_betaiotaevar_preserving_vm_cast Gravatar jforest2006-04-14
* MAJ 8.1-APPGravatar herbelin2006-04-13
* MAJ 8.1-APPGravatar herbelin2006-04-13
* Changement de licence pour le Tutoriel de CoqGravatar notin2006-04-12
* Simplifying the proof of principlesGravatar jforest2006-04-12
* induction on multiple arguments made better:Gravatar courtieu2006-04-12
* Modification of "Show Intros": it now shows letins too.Gravatar courtieu2006-04-11
* adding a new tactic [intro_avoiding idl] which acts as intro but prevents theGravatar jforest2006-04-11
* ajout d'entrées dans TODO et CHANGES (à re-mettre à jour avant la release)Gravatar courtieu2006-04-11
* patch pour contourner l'échec de type_of_applied_inductive sur un inductif a...Gravatar herbelin2006-04-11
* Fixes for new unification, not used in default version as it really changes u...Gravatar msozeau2006-04-10
* + Changing a little functional schemes types Gravatar jforest2006-04-10
* Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...Gravatar msozeau2006-04-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 23:06:31 +0000