index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
translate
Commit message (
Expand
)
Author
Age
*
Mise en place possibilité de définitions locales dans les paramètres des r...
herbelin
2003-09-06
*
Paramétrisation vis à vis de existential_key
herbelin
2003-09-06
*
Mise en place possibilité de définitions locales dans les paramètres des i...
herbelin
2003-09-06
*
Mise en place possibilité de définitions locales dans les paramètres des i...
herbelin
2003-09-06
*
Passage de lconstr à constr pour les arguments immédiat de commandes
herbelin
2003-09-06
*
Affichage des 'fun' suivis de 'let' en utilisant explicitement un 'let'
herbelin
2003-09-03
*
Contorsions pour que l'interpretation deses foncteurs depende des parametres ...
herbelin
2003-09-02
*
Bug traduction Search, SearchPattern, etc.
herbelin
2003-09-02
*
Bug et améliorations divers
herbelin
2003-08-31
*
Amélioration affichage syntaxe modules
herbelin
2003-08-14
*
Hack pour ajouter Proof apres Correctness
herbelin
2003-08-13
*
Bug et amliorations diverses
herbelin
2003-08-12
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Ajout systématique de Proof dans la traduction
herbelin
2003-06-23
*
Formattage Apply with
herbelin
2003-06-23
*
Formattage pattern 'match'
herbelin
2003-06-23
*
Ajout 'Symmetry in Hyp'; chgt syntaxe 'change ... with ...'
herbelin
2003-06-19
*
Ajout option Local à Hint, Hints et HintDestruct
herbelin
2003-06-14
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
Ajout option translate_syntax pour caractériser l'interprétation du traduct...
herbelin
2003-06-12
*
Ajout notation c.(f) en v8 pour les projections de Record; raffinement divers
herbelin
2003-06-10
*
Raffinement divers
herbelin
2003-06-10
*
Globalisation des tactiques avant traduction pour capture des noms; affinemen...
herbelin
2003-06-10
*
Ajout FreshId
herbelin
2003-05-24
*
Ajout V8Notation
herbelin
2003-05-22
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...
herbelin
2003-05-21
*
Possibilité de syntaxe conjointement à la définition des inductifs et des ...
herbelin
2003-05-21
*
Prise en compte notation dans Inductif pour traducteur
herbelin
2003-05-20
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Separation entre les propositions de syntaxe - suite
herbelin
2003-05-13
*
Separation entre les 2 propositions de syntaxe
herbelin
2003-05-13
*
coqide: toolbar/autosave
monate
2003-05-07
*
Prise en compte des syntaxes v8 dans Uninterpreted Notation
herbelin
2003-04-29
*
Factorisation des produits de même type; parenthèses autour des x:=c et n:=...
herbelin
2003-04-29
*
Localisation erreurs TacAlias; Globalisation moins tolérante dans les
herbelin
2003-04-28
*
Reparation affichage LetTac
herbelin
2003-04-27
*
Ajout "at next level" dans Notation
herbelin
2003-04-17
*
Localisation des appels de tactiques définies sans arguments
herbelin
2003-04-14
*
Ajout option 'Local' à Infix et Notation
herbelin
2003-04-11
*
Affichage des inductifs
herbelin
2003-04-10
*
Affichage des inductifs
herbelin
2003-04-09
*
Formattage affichage
herbelin
2003-04-09
*
Mécanisme plus simple et efficace pour traduire les implicites
herbelin
2003-04-09
*
Bugs synchronisation pour gestion traduction des implicites
herbelin
2003-04-09
*
Réorganisation de Impargs + mise en place d'une infrastructure
herbelin
2003-04-09
*
Ajout option "Local" à "Open Scope"
herbelin
2003-04-08
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Aérer les := et : de "assert"
herbelin
2003-04-07
*
Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun implicite
herbelin
2003-04-07
[next]