aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2005-03-06majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6803 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-06the package script disappeared in MacOS 10.3: we locally copy the 10.2 versionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6799 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-05majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6797 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-04majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6795 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-03majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6793 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6791 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-01majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6789 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-01clean de parser.optherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6788 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-01Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6787 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-01MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6786 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-28majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6784 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-27majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6782 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-26majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6780 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-25majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6778 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6776 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-23majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6774 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-23quelques tactics ltacletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6773 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-22majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6771 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-22Suppression des fichiers temporairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6769 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-21majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6767 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-21majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6766 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-21*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6765 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-21Pas de dépendance en Omegaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6764 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-21Correction de bugs: coq_false et coq_true au lieu de coq_False et coq_trueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6763 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-21- changement ordre arguments interp_goal_concl pour permettre applicationherbelin
partielle - amélioration traduction en nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6762 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-21- Correction de bugsherbelin
- filtrage sur Bigint.zero incorrect: zero était considéré comme une variable - coq_false et coq_true au lieu de coq_False et coq_true - vérification chargement ROmega.vo - Divers - changement ordre argument interp_goal_concl pour permettre application partielle - amélioration débogueur - ajout interprétation Zsucc, Zopp, et gel de Zmult si non scalaire git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6761 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-20majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6759 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-20Keep ClosedSection marker for resetherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6758 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-19majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6756 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6754 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6753 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving subst_inductive from tacinterp to inductiveops for better for reuse ↵herbelin
in recordops git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6752 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving centralised discharge into dispatched discharge_functionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6751 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Renaming Print Canonical Structure into Print Canonical Projectionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6750 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ↵herbelin
delay some computation from before to after caching time + various simplifications and uniformisations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6749 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ↵herbelin
delay some computation from before to after caching time + various simplifications and uniformisations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Standardisation of constr_of_reference into constr_of_global + Moved Indmap ↵herbelin
and ConstrMap to Names git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6747 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Standardisation of function names about structuresherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6746 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Standardisation of function names about global references (especially, ↵herbelin
renaming of constr_of_reference into constr_of_global) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6745 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ↵herbelin
delay some computation from before to after caching time + simplifications and uniformisations + Renaming Print Canonical Structure into Print Canonical Projections git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6744 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ↵herbelin
delay some computation from before to after caching time + exporting whether a projection is a true projection or a constant associated to a let in the type of the record constructor (fix a bug for canonical structures with let's) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6743 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Déboggueur et code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6742 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving subst_inductive from tacinterp to inductiveops for better for reuse ↵herbelin
in recordops git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6741 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Ajout it_mkNamedProd_wo_LetInherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6740 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Ajout splay_lambdaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6739 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6738 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Added map_named_contextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6737 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moved Indmap and ConstrMap from Libnames to Names for use in Cookingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6736 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Ajout constant printerherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6735 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18q_*.cmo useless for making coqtopherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6734 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 16:33:22 +0000