aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
...
* Indépendance vis à vis de Symbols (suite)Gravatar herbelin2004-11-27
* Bug commit 1.71Gravatar herbelin2004-11-22
* Correction bug Notation: il faut re-déclarer les règles de parsing des nota...Gravatar herbelin2004-11-22
* compatibility with POWERPCGravatar gregoire2004-11-22
* 'Rewrite' mot-clé pour que 'Print Rewrite HintDb' marcheGravatar herbelin2004-11-20
* New command "Print Rewrite HindDb dbname".Gravatar sacerdot2004-11-17
* Ajout 'Locate Module'Gravatar herbelin2004-11-17
* Déclaration de '..' comme mot-clé (résoud bug #856)Gravatar herbelin2004-11-17
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* Correction bug #868Gravatar herbelin2004-11-10
* Univ.pr_univ ==> Univ.pr_uniGravatar sacerdot2004-11-04
* Affichage des universGravatar herbelin2004-11-04
* Bug mauvais nom d'entrée binder_constr quand récursion gaucheGravatar herbelin2004-10-27
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Desactivation de la construction 'lazy match' en attendant une autre solutionGravatar herbelin2004-10-12
* Mise en conformité de la syntaxe de Theorem/Lemma avec la doc: les lieurs so...Gravatar herbelin2004-10-12
* Réinstallation des lieurs avant l'énoncé de Theorem/Lemma (non documenté ...Gravatar herbelin2004-10-12
* 'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...Gravatar herbelin2004-10-11
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* Ajout de or-pattern pour le match-with v8Gravatar herbelin2004-09-09
* Meilleur anglais (cf #841)Gravatar herbelin2004-09-08
* deplacement de clenv vers pretypingGravatar barras2004-09-03
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Dépendance en pa_ifdef dans la ligne camlp4deps de q_coqast induit make depe...Gravatar herbelin2004-08-26
* Précisions message d'erreurGravatar herbelin2004-08-23
* Distinction location ocaml 3.08 ou pas (suite)Gravatar herbelin2004-07-29
* Distinction location ocaml 3.08 ou pasGravatar herbelin2004-07-29
* Bug tactique fixGravatar herbelin2004-07-28
* "Print Setoids" command added.Gravatar sacerdot2004-07-23
* Abstraction vis à vis de dummy_locGravatar herbelin2004-07-20
* Abstraction vis à vis du type loc pour compatibilité ocaml 3.08Gravatar herbelin2004-07-16
* Suppression quotifyGravatar herbelin2004-07-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* Branchement sur Util.loc et abstraction vis a vis de dummy_locGravatar herbelin2004-07-16
* Abstraction vis a vis de dummy_locGravatar herbelin2004-07-16
* bugs #667 and #783 (mimick_evar and loc_table on large files)Gravatar barras2004-07-13
* moved instantiate binding to extratacticsGravatar corbinea2004-06-29
* efficacite du lexeurGravatar filliatr2004-06-29
* more evar stuffGravatar corbinea2004-06-28
* Nouvelle syntaxe à la ML pour donner le type ML des extensions d'argumentsGravatar herbelin2004-06-17
* Affichage de l'opacité par About mais pas par Print (compatibilité coq'art)Gravatar herbelin2004-06-03
* Affichage de l'opacité dans Print et AboutGravatar herbelin2004-06-02
* Bug affichage ClearBodyGravatar herbelin2004-05-27
* Bug syntaxe AddPathGravatar herbelin2004-05-14
* Ajout entree pour exporter les commentaires en mode -xmlGravatar herbelin2004-03-26
* Code mortGravatar herbelin2004-03-25
* Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...Gravatar herbelin2004-03-17
* Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...Gravatar herbelin2004-03-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 02:19:39 +0000