aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2005-02-18Added bigint printerherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6733 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6731 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6730 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-17Test bug #922herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6729 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-17Correction bug #922 (problème dans depend) + formattage débogueurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6727 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-17Bug affichage entiers négatifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6726 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-16majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6724 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-15majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6722 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-14majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6720 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-13majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6718 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6716 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6715 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12Nouvelle mouture Print Canonical Structuresherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6714 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12Uniformisation de destApplication en destAppherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6713 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12Uniformisation de destApplication en destApp; simplification decompose_appherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6712 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12Ajout Print Canonical Structuresherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6711 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-11majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6709 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-10majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6707 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-10Ajout du reset des numéros d'états dans reset_initial. Plus proprecoq
pour proofgeneral. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6706 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-09majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6704 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-08majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6702 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6700 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-07Re-unboxing de BinPos (sauf Pplus): sinon, fait partir Coqbook pour des ↵coq
jours de calcul (chapitre 16, thm prime_2333); peut-être à cause de Z_of_nat??) [HH] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6699 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-02 05:47:37 +0000