aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-01-20Ajout de la contrainte de résoudre l'assertion dans 'assert by'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7902 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-20Test bug 983herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7901 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-20*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7899 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-19majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7896 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-19Conséquences supplémentaires de la fin du support v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7895 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-19Export eassumptionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7894 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-19Extended Unicode supportherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7893 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-19Correction associativité de IF et exists (visible à l'affichage uniquement ↵herbelin
à cause du traitement spécial du niveau binder_constr) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7892 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-18majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7889 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-18Retrait de 'by' comme mot-clé en espérant qu'il n'y aura pas ↵herbelin
d'interférence avec des notations utilisateurs qui le remettrait mot-clé plus tard git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7888 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-18Recursive Definition now supports functions with more than one argument.coq
Julien git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7887 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7885 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7883 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16dans la liste des cmo pour dev/printers.cma, manquait proofs/tacexpr.cmoletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7882 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16Version préliminaire d'inversion de la compilation du filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7881 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coqherbelin
choisir un nom; utilisation de IntroAnonymous au lieu de None dans l'argument "with_names" des tactiques induction, inversion et assert. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7880 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nomherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7879 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16*** empty log message ***coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7878 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16Code redondantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7877 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16Correction dans vernac_exact_proof -- jmncoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7876 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16- Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesherbelin
- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns - TacTrueCut and TacForward merged into new TacAssert bound to Tactics.forward git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7875 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16cvs ci -m "Passage à la limite dans les intro-pattern de n-uplets"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7874 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-15majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7871 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-15Ajout de nouvelles plages de symboles unicode; prise en compte des indices ↵herbelin
unicode et letter-like dans les identificateurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7870 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-15Bug (code prévu pour iso-latin et non utf-8)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7869 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-15Test utf-8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7868 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-14majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7866 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-14Code mort du traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7865 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-13majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7863 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-13Correction du bug #1055coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7862 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-12majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7857 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-12Changing well founded induction to fix on accessibility proof in orderbertot
to prepare the possibility to define function with more that one argument. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7856 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-12Compatibilité prtermherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7855 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7852 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Test conflictuel - ajouté pour mémoireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7849 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Test or-patternsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7848 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Ajout test notation récursiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7847 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Suppression traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7846 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11remove warnings that were left in the directory contrib/interfacebertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7844 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11removes several warnings in contrib/interfacebertot
Modifies the behavior of Recursive definition to produce goals instead of established theorems git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7843 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Résidus du traducteur v7 -> v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7842 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Standardisation du nom de subst_raw en subst_rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7841 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Suite réorganisation des fonctions d'affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7840 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Standardisation du nom de subst_raw en subst_rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7839 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Résidus du traducteur v7 -> v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7838 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Ajout paramétricité du nom de la base de hint dans auto et trivialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7836 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Ajout paramétricité du nom de la base de hint dans auto et trivialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7835 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Suppression résidus code v7 et traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7834 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-10Ajout de la longueur de l'arité des constructeurs dans one_inductive_body ↵herbelin
et dans case_info pour permettre l'indépendance de detyping (entre autres) envers l'environnement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7833 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 06:25:48 +0000