aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Collapse)Author
2001-08-06Nouvelle entrée ident_or_numargherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1881 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Mise en place d'un nouveau Destruct sur le modèle du nouvel Inductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1874 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-19Changements dans le traitement des qualid'sdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1859 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-19modifs de preuves (plus simples)mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1858 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-13reparation regles pour parsing Coercion Localmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1849 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-04ajout Show Intro(s)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1825 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-02Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans ↵herbelin
Compute, nouveaux flags utilisateurs pour Evar et Zeta git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1820 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-02Ajout glob_eq{,T}herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1818 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la ↵herbelin
définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1806 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la ↵herbelin
compilation native powerpc), le nouveau morceau étant g_ltac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1803 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-19Extension des parametres de Clear + Instdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1794 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-18Interpretation MetaId + Progress + Instdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1789 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-11Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Caseclrenard
n'etaient pas affiches correctement lors du Save si on les avait donne en argument de tactique. Avec Bruno, nous avons simplifie l'ast en remplacant les MLCASE NOREC et autres CASE NOREC par des choses plus simples. Il y a maintenant un noeud LET, un IF, un CASE et un MATCH qui sont a peu pres semblables mais qui permettent de se souvenir quoi afficher. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1781 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-11Fix de quelques bugs syntaxiques de Ltacdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1780 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-29Retablissement de minicoqcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1773 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-29Facilites pour le debogguage des univers.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1772 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-28Pretty -> Prettypfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1768 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-03Changement de la structure des points fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-25message d'erreur pour rattrapper l'anomalie avec SQUASHbarras
Check {True}. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1719 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-25Amelioration affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1707 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Messages d'erreur Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1703 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Les clauses de Rec doivent prendre des tactic_atom'sdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1701 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23un warning pas beau supprimméfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1669 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Petit menagedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1642 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19*** empty log message ***mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1610 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Essais dans Ltacdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1606 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-15Bug affichage d'implicites pour les vars lieesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1593 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-14Non parenthesage des applications de tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1590 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-12Ajout de _ dans les patterns d'intromohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1584 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-10Modified searchPattern. Before this correction, constructors were overlooked,bertot
because the observation was done on the internal data-structure provided in the inductive definition. But this internal data-structure is not well-suited pattern-matching, since it contains debruijn indices where the inductive type should occur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1572 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-09Uniformisation des 'Save def_tok id'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1564 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-09nettoyage d'entrees de grammaires inutilescourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1563 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-09branchement extraction en standard (pas de Require)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1561 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-06bug Print Proof; usage coqtop/coqcfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1552 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-05mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1551 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug ↵filliatr
d'ocamldep git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1547 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04Add a flag to avoid sending too many warnings when reloading syntax filesbertot
in the parser used for the graphical user-interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1541 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04adding entry points for the arguments of the Comment command.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1534 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04Adding A command for comments, this makes it possible to have structuredbertot
comments that will be displayed nicely in structured oriented interfaces like pcoq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1533 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-03The function filter_by_module, that was previously exported was not thebertot
one that was really needed. I changed it for filter_by_module_from_list git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1525 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-03Export a function (build_inductive) that is used in the graphical interface.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1524 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30branchement extraction (bytecode seulement)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1509 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-28amelioration de la structure des universbarras
elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23amelioration de la consommation memoire de la conversion en eta-expansantbarras
les definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1483 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-22Bug MUTCASE au lieu CASEherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1476 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-11Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1447 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-16Bug affichage coercionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1396 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1395 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-12 10:46:20 +0000