aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-08-10Repository : pauillac.inria.fr:/net/pauillac/constr/ARCHIVEherbelin
Module : CONSTR/V7 Working dir: ~/V7uo/ In directory .: Modified .depend Modified CHANGES Unknown COMMIT Modified Makefile Modified TODO Unknown log.up Unknown parsing-sans-slam Unknown titi.v Unknown toto.v In directory contrib: Unknown contrib/interface_essai Unknown contrib/log In directory contrib/correctness: Modified contrib/correctness/pcic.ml Modified contrib/correctness/pmisc.ml Modified contrib/correctness/psyntax.ml4 In directory contrib/extraction: Modified contrib/extraction/extract_env.ml Modified contrib/extraction/haskell.ml Modified contrib/extraction/ocaml.ml Modified contrib/extraction/ocaml.mli In directory contrib/field: Modified contrib/field/field.ml4 Message: cvs server: New directory `contrib/interface' -- ignored Unknown contrib/interface/ctast.ml In directory contrib/omega: Modified contrib/omega/coq_omega.ml In directory contrib/ring: Modified contrib/ring/Setoid_ring_normalize.v Modified contrib/ring/quote.ml Modified contrib/ring/ring.ml Message: cvs server: New directory `contrib/setoid' -- ignored In directory contrib/xml: Modified contrib/xml/xmlcommand.ml In directory dev: Modified dev/base_include Modified dev/top_printers.ml In directory kernel: Modified kernel/cooking.ml Modified kernel/cooking.mli Modified kernel/environ.ml Modified kernel/environ.mli Unknown kernel/identifier.ml Unknown kernel/identifier.mli Modified kernel/names.ml Modified kernel/names.mli Modified kernel/safe_typing.mli Modified kernel/univ.ml In directory lib: Modified lib/system.ml Modified lib/system.mli Modified lib/util.ml Modified lib/util.mli In directory library: Modified library/declare.ml Modified library/declare.mli Modified library/global.ml Modified library/global.mli Modified library/lib.ml Modified library/lib.mli Modified library/library.ml Modified library/library.mli Modified library/nametab.ml Unknown library/nametab.ml.copie Unknown library/nametab.ml.saved Modified library/nametab.mli Unknown library/nametab.mli.saved In directory parsing: Modified parsing/ast.ml Modified parsing/ast.mli Modified parsing/astterm.ml Modified parsing/coqast.ml Modified parsing/coqast.mli Modified parsing/coqlib.ml Modified parsing/coqlib.mli Modified parsing/esyntax.ml Modified parsing/extend.ml4 Modified parsing/g_basevernac.ml4 Modified parsing/g_cases.ml4 Modified parsing/g_constr.ml4 Modified parsing/g_ltac.ml4 Modified parsing/g_prim.ml4 Modified parsing/g_rsyntax.ml Modified parsing/g_tactic.ml4 Modified parsing/g_vernac.ml4 Modified parsing/g_zsyntax.ml Modified parsing/lexer.ml4 Modified parsing/pcoq.ml4 Modified parsing/pcoq.mli Modified parsing/pretty.ml Modified parsing/prettyp.ml Modified parsing/printer.ml Modified parsing/q_coqast.ml4 Modified parsing/search.ml Modified parsing/termast.ml In directory pretyping: Modified pretyping/classops.ml Modified pretyping/syntax_def.ml In directory proofs: Modified proofs/proof_trees.ml Modified proofs/tacinterp.ml Modified proofs/tacinterp.mli In directory tactics: Modified tactics/Inv.v Modified tactics/dhyp.ml Modified tactics/inv.ml Modified tactics/inv.mli Modified tactics/setoid_replace.ml Modified tactics/tacticals.ml Modified tactics/tactics.ml Modified tactics/tauto.ml4 In directory test-suite: Unknown test-suite/vernac In directory theories: Message: cvs server: New directory `theories/Zarith' -- ignored In directory toplevel: Modified toplevel/class.ml Modified toplevel/command.ml Modified toplevel/command.mli Modified toplevel/coqinit.ml Modified toplevel/coqtop.ml Modified toplevel/discharge.ml Modified toplevel/discharge.mli Modified toplevel/mltop.ml4 Modified toplevel/record.ml Modified toplevel/vernacentries.ml Modified toplevel/vernacinterp.ml --------------------- End --------------------- -- last cmd: cvs -f -n update -d -P -- git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1888 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-08Renommage TrueCut -> Assertherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1887 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-08Ajout nf_betaiota dans le cut interneherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1886 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-08La grammaire n'était plus LL1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1885 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-08Modification Tauto pour qu'il puisse destructurer des hypotheses de la formecourant
e1 -> e2 avec e1 type inductif ayant un unique constructeur constant. Cas typique : hypothese de la forme ~e=e. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1884 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-07Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ↵herbelin
tactique primitive Cut basé sur un Let non dépendant; amélioration efficacité ancien Cut git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1883 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-07Passage au nouveau Destructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1882 85f007b7-540e-0410-9357-904b9bb8a0f7
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-05Expérimentation de NewDestruct et parfois NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1880 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1879 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas ↵herbelin
s'appliquer au but; appel optionnel de Intros Until sur certaines tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1878 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Elimination des coupures quand les 'clause' se réduisent à des ↵herbelin
hypothèses, nouveau combinateur onHyps git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1877 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Ajout error_global_not_foundherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1876 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas ↵herbelin
s'appliquer au but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1875 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-08-05Suppression des TmpHyp disgracieuses dans Decompose; utilisation de ↵herbelin
combinateurs sur les hyps plutôt que sur les clauses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1873 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Elimination des coupures quand les 'clause' se réduisent à des ↵herbelin
hypothèses, nouveau combinateur onHyps git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1872 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Nouveau profiler compatible avec ocaml >= 3.01herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1871 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-01Ajout code pour un Destruct similaire au NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1870 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-01Ajout make_elimination_identherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1869 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-01Ajout add_prefix/add_suffixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1868 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-01Ajout profile dans PARSERREQUIRE, nécessaire si certaines fonctions d'un ↵herbelin
des autres fichiers de PARSERREQUIRE est profilé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1867 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-01MAJ vis à vis de ocaml 3.01herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1866 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-24Suppression de l'affichage du non-reparsable 'Local constraint change'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1865 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-24Bug Simplherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1864 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-23Comentaire errone.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1863 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-21Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ↵herbelin
par le nombre d'args inutiles + vérification dans le noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1862 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-21Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1861 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-21Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ↵herbelin
par le nombre d'args inutiles + vérification dans le noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1860 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-18Ajout de la contrib sur les graphesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1857 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-17"make clean" nettoie les .g all.ps all-gal.ps et les fichiers HTMLfilliatr
générés à partir des .v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1856 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-16all.g.ps -> all-gal.psfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1855 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-16compat -sort et -suffixfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1854 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-16cibles all.ps et all-gal.ps (utilisation de coqweb)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1853 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-16utilisation de printf (simplif)filliatr
option -sort pour trier les .v selon les dépendances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1852 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-16modif Map sectionmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1851 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-16Nettoyagemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1850 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-13Branchement de induction/destruct sur intros_until_n (intros_do obsolete ne ↵herbelin
prend pas les letin en compte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1848 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Setoid_rewrite -> Rewriteclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1847 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Branchement sur bad_tactic_argsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1846 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Branchement sur bad_tactic_argsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1845 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Ajout des fichiers pour le Ring pour setoidesclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1844 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Ajout du .ml pour la tactique Setoid_replaceclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1843 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Ajout du .v pour la tactique Setoid_replaceclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1842 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Changement de place de la tactique Setoid_rewrite et renommageclrenard
en Rewrite. Le choix entre egalite de Leibnitz et egalite de setoide est fait automatiquement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1841 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Changement de place de la tactique Setoid_rewriteclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1840 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Ajout d'un Ring pour setoidesclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1839 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-24 03:37:35 +0000