aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Bug compilationGravatar herbelin2003-06-20
* Ajout 'Symmetry in Hyp'Gravatar herbelin2003-06-19
* Ajout 'Symmetry in Hyp'; chgt syntaxe 'change ... with ...'Gravatar herbelin2003-06-19
* Ajout option Local aux HintGravatar herbelin2003-06-17
* Ajout option Local à Hint, Hints et HintDestructGravatar herbelin2003-06-14
* Utilisation de intro_pattern dans NewDestruct/NewInductionGravatar herbelin2003-06-13
* Token '.(' seulement pour v8, sinon conflit avec '.(*'Gravatar herbelin2003-06-11
* Ajout notation c.(f) en v8 pour les projections de RecordGravatar herbelin2003-06-10
* freshid -> freshGravatar herbelin2003-06-10
* Tables logarithmiques pour les coercions + nettoyageGravatar herbelin2003-06-08
* BugGravatar herbelin2003-05-26
* Ajout FreshIdGravatar herbelin2003-05-24
* Ajout V8NotationGravatar herbelin2003-05-22
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
* Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...Gravatar herbelin2003-05-21
* Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...Gravatar herbelin2003-05-21
* Possibilité de syntaxe conjointement à la définition des inductifs et des ...Gravatar herbelin2003-05-21
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Petite correction d'affichage de modulesGravatar coq2003-05-08
* Prise en compte des syntaxes v8 dans Uninterpreted NotationGravatar herbelin2003-04-29
* Prise en compte des syntaxes v8 dans Uninterpreted NotationGravatar herbelin2003-04-29
* Factorisation des produits de même type; parenthèses autour des x:=c et n:=...Gravatar herbelin2003-04-29
* Factorisation des produits de même type; parenthèses autour des x:=c et n:=...Gravatar herbelin2003-04-29
* Ajout is_ident_tailGravatar herbelin2003-04-29
* Localisation erreurs TacAlias; Globalisation moins tolérante dans lesGravatar herbelin2003-04-28
* Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...Gravatar herbelin2003-04-27
* Reparation affichage LetTacGravatar herbelin2003-04-27
* extension des caracteres UTF 8 autorises dans les symbolesGravatar filliatr2003-04-25
* Ajout "at next level" dans NotationGravatar herbelin2003-04-17
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...Gravatar letouzey2003-04-16
* Localisation des appels de tactiques définies sans argumentsGravatar herbelin2003-04-14
* Correction bug PR#278Gravatar coq2003-04-14
* Ajout option 'Local' à Infix et NotationGravatar herbelin2003-04-11
* Affichage forcé des implicites contextuels si pas de contexte connuGravatar herbelin2003-04-10
* Réorganisation de Impargs + mise en place d'une infrastructureGravatar herbelin2003-04-09
* Ajout option "Local" à "Open Scope"Gravatar herbelin2003-04-08
* lconstr pour genterm en v8Gravatar herbelin2003-04-07
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Ajout cas MatchGravatar herbelin2003-04-07
* Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun impliciteGravatar herbelin2003-04-07
* Options d'affichage maintenant dans ConstrexternGravatar herbelin2003-04-07
* espace manquantGravatar herbelin2003-04-02
* Ajout d'un message à FailTacGravatar herbelin2003-03-31
* Bug pattern_occ_hyp_listGravatar herbelin2003-03-31
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29
* notations <>, Assumption avec existentiel, replace termGravatar mohring2003-03-28
* MAJ des mots-clés, Definition, Theorem, ...Gravatar herbelin2003-03-27
* MAJ des mots-clés, Definition, Theorem, ...Gravatar herbelin2003-03-27
* Affinement nommage des productionsGravatar herbelin2003-03-27
* *** empty log message ***Gravatar barras2003-03-21