aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Collapse)Author
2002-05-14Utilisation d'une construction spéciale SECVAR pour gérer laherbelin
globalisation des variables de section (en espérant plus de robustesse vis à vis des bugs récurrents de Infix pour les variables avec implicites) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2684 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-10Plus de souplesse pour les constructeurs encapsulés sous des définitionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2674 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-18Suppression d'un warning plus surprenant qu'utileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2658 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-16Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2647 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-10Amélioration des messages d'erreurs concernant l'inférence des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2630 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-10Syntactic Definition autorisée dans les motifs de Cases (utile notammentherbelin
pour fusionner eq et eqT) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2628 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-02- modifs de la condition de garde pour mieux tenir compte des raisonnementsbarras
par l'absurde - un open_constr est maintenant un terme accompagne du sigma dans lequel il est typable (il manquait l'info concernant le contexte de typage des nouvelles evars) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2579 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-29Correction bug infix sur des varaiablesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2577 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-19Ajout de l'entrée ne_constrarg_listdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2543 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-17Meilleure gestion de la reduction dans Fielddelahaye
Field term (nouveau) Injections dans l'interpreteur de tactiques Exportation de quelques entrees de grammaires Exportation de quelques fonctionnalites des definitions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2538 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14option -dump-glob pour coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-11substitution et pattern modulo letbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2466 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-07petit nettoyage de kernel/inductivebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-01Ajout tactiques Rename et Pose; modifications pour Inversionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2449 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-31changement generation de schema d'elimination, False_rec est primitif, ↵mohring
Constructor tac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2447 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18Plusieurs arguments autorisés pour Require et Read Moduleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2412 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-21Bug affichage '++' au lieu de ';'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2364 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Modif précédente trop violente (cf test-suite/success/CasesDep.v)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2341 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18On ne peut plus appliquer des arguments à une syntaxe primitiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2317 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18affichage correct du type des inductifs et constructeurs en presencebarras
de parametres git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2312 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18parsing des branches de Cases au niveau lconstr (au lieu de constr)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2306 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-16Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + ↵herbelin
suppression des @Coercion, @Local et @Local Coercion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2299 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13MAJ de la traduction en ast des variables de section en qualidherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2296 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-10- condition de garde (suite)barras
- commande Back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2283 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29nouvel algo de conversion plus uniformebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-23Retablissement de la commande Existential que j'avais supprime par erreur.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2243 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20types vs constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2213 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Diverses petites simplications de la machine de preuves.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2204 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Re-installation de l'affichage des globaux par des noms courtsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2200 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-08Prise en compte de la syntaxe [x:=c:t]b comme équivalent de [x:=c::t]bherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2170 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-24Suppression de Logic_Type.sigT, redondant avec Specif.sigTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2139 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-23Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2136 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre ↵herbelin
sens pour plus de partage entre chemins git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-15Nouvelle correction du bug confusion entre implicites de locaux et de globauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2115 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-12Déplacement de global_reference dans Names pour pouvoir lier Nametab à ↵herbelin
grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2112 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-11Bug collision entre les implicites d'un global et les variables locales de ↵herbelin
même nom court git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2108 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-05Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs ↵herbelin
'ClearBody H' et 'Assert H := c' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2104 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-02Ajout de dynamiques pour les quotations constr et tacticdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2093 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-24Marre des unrecognized objectsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2055 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21Réparation des options Set Printing and coherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2052 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21Mise en place globalisation optionnelle pour Infix/Distfixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2046 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Amélioration affichage de print_leaf_entryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2040 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Rajout 'Set Printing Depth'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2039 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Transparentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 16:11:39 +0000