aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface
AgeCommit message (Expand)Author
2003-11-25Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...herbelin
2003-11-18correction suite ajout nouvelles tactiquesclrenard
2003-11-15Ajout Print Implicit avec depliage du typeherbelin
2003-11-13factorisation et generalisation des clausesbarras
2003-11-12Bug TacIdherbelin
2003-11-10Suppression SearchNamed finalement redondant avec SearchAboutherbelin
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
2003-11-06Added Instantiate ... incorbinea
2003-11-01Ajout CPatNotation, PrintVisibilityherbelin
2003-10-23Conjecture declare maintenant un axiome; reorganisation VernacDefinitionherbelin
2003-10-22Integration de SearchNamed dans SearchAboutherbelin
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
2003-10-16nouvelle syntaxe de ltacbarras
2003-10-13Ajout d'une fonction de recherche sur les composantes du nom des objetsherbelin
2003-10-13Deplacement next_global_ident_away dans Termopsherbelin
2003-10-13Ajout d'une fonction de recherche sur les composantes du nom des objetsherbelin
2003-10-10Cablage en dur de inversionherbelin
2003-10-10show_subgoals dans Pfeditherbelin
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-10-08Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...herbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-09-30Ajout 'Close Scope', mise en place de la structure pour un modificateur 'format'herbelin
2003-09-23Utilisation de noms dans 'Implicit Arguments [...]'herbelin
2003-09-21Mise en place d'implicites par noms en v8herbelin
2003-09-19parsingherbelin
2003-09-12Ajout 'Print Scopes' et 'Bind Scope with classes'herbelin
2003-09-09Ajout construction If primitive dans constr_expr et rawconstrherbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des r...herbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des i...herbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-06-19Ajout 'Symmetry in Hyp'herbelin
2003-06-14Ajout option Local à Hint, Hints et HintDestructherbelin
2003-06-13Utilisation de intro_pattern dans NewDestruct/NewInductionherbelin
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-05-21MAJherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-04-28Localisation erreurs TacAlias; Globalisation moins tolérante dans lesherbelin
2003-04-17Ajout "at next level" dans Notationherbelin
2003-04-11Ajout option 'Local' à Infix et Notationherbelin
2003-04-09Réorganisation de Impargs + mise en place d'une infrastructureherbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-03-31Ajout d'un message à FailTacherbelin
2003-03-31factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )corbinea
2003-03-12*** empty log message ***barras
2003-03-10Remove a TODO in the translation of generic arguments:bertot
2003-03-06Make sure that identifiers are parsed as qualified identifier and thatbertot
2003-02-05Ajout du traducteurdesmettr
2003-02-03Added a clause for VernacDefineModule, but with an error as result.bertot
2003-01-26all tactics should be covered now: remainsbertot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:14:36 +0000