aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2007-06-30Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Recordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9918 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-30- Ajout de la possibilité d'utiliser la notation Record pour lesherbelin
coinductifs à un constructeur (suggestion de Georges). - Si pas de sorte ou arité mentionnée dans Inductive/CoInductive/Record, Type est utilisé comme défaut. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9917 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-29Added the directory theories/Numbers where axiomatizations and ↵emakarov
implementations (unary, binary, etc.) of different number classes (natural, integer, rational, real, complex, etc.) will be stored.Currently there are axiomatized natural numbers with two implementations and axiomatized integers. Modified Makefile accordingly but dod not include the new files in THEORIESVO yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9916 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-27- Extensions of FMap(Weak)Facts: letouzey
fold properties and induction principles for (weak) maps. - Simplification in SetoidList: the two important results fold_right_equivlistA and fold_right_add are now proved without using removeA and hence do not depend anymore on a decidable equality (good for maps and their arbitrary datas). In fact, removeA is not used at all anymore, but I leave it here (mostly), since it can't hurt. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9914 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-27eqlistA is now equivlistAletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9913 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-26killing some more non-exhaustive patternsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9912 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-26kill an ugly warning about a non-exhaustive patternletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9911 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-26Oups: thanks to ./configure -reals no, I was not building the whole ↵letouzey
dependencies for the coq files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9910 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-26Added zwqipWith.roconnor
Added theory about intractions between nth and map, and zipWith. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9909 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-26additional properties for FMap (and slight rework of SetoidList and ↵letouzey
FSetProperties) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9908 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-25Updated Qpow_tac to work on a a more realistic set of exponent values.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9907 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-22Ajout exist & cie à la table des hints par symétrie avec ex_intro &herbelin
cie (cf message coq-club 21/6/07). De plus, left/right inleft/inright, eux aussi dans Set/Type, y étaient déjà donc l'argument d'être dans Type n'est pas recevable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9906 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-21Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc, notin
et une typo dans Eqdep_deq.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9905 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-21Simplification de la construction du .depend:notin
- make ou make world entraînent la construction de .depend et .depend.coq; - suppression des cibles .depend et .depend.coq (au profit de depend et dependcoq) - suppression de la dépendance de depend avec les .ml (inutile) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9904 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-21Correction de plusieurs bugs de l'export XML (utilisation d'un type deherbelin
constante par defaut pour les nouveaux types plutot qu'echouer; avertissement plutot qu'echec en cas de foncteur; nommage systematique des LetIn -- p.ex. functional induction engendre des LetIn non nommes --; branchement de la fonction de normalisation de tete evitant CProp sur Closure au lieu de Tacred afin de garantir la f.n. de tete) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9902 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-21Adding: Field instance for Q.roconnor
: Power function from Q -> Z -> Q. : Absolute value function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9901 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-20ajout de head0 et tail0 en natifbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19safe_shift correct recursionthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9899 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19safe_shift recursionthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9898 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19safe_shift recursionthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9897 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19typo faqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9895 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19Adding function is_even, safe_shiftl, safe_shiftrthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9894 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19genN.ml syncthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9893 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-18Correct height computationthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9892 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-14oups: one file forgotten in my previous commitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9891 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-14Rework of FSetProperties, in order to add more easily a Properties functor letouzey
for FMap (for the moment in FMapFacts). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9890 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-14Correction du bug sur make dependnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9889 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-14Add Solve All Obligations command, fix bug in inequality generation ↵msozeau
introduced by previous commit, add general purpose tactics for destructing existentials and disjunctions. Compiles without camlp4 warnings too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9888 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-11undeletion of E_ST and Equal_ST: these records aren't mandatory, but quite ↵letouzey
useful git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9887 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-09Various Program fixes, multiple pattern matches, aliases. Fix bug in ↵msozeau
coercion code for simultaneous coercion of different arguments of an inductive type. Add tactics for dealing with heterogeneous equality. Export more error reporting functions from Cases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9886 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-08some more properties of fold and elements in FSetPropertiesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9885 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-08Removed an extra \tacindex occurrence for the tactic discriminate.emakarov
Added a tactic "now" which is nonrecursive but generalizes "trivial". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9884 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-07Extension of NArith: Nminus, Nmin, etcletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9883 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-07* For uniformity, FSetAVL uses Implicit Arguments (a bit)letouzey
* Some additionnal properties: - two more induction principles on sets - some results about union, filter, etc - Subset is declared to be a Setoid Relation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9882 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-07Ajout doc clear sans argumentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9880 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-07Unification des types + clause filtrage manquante + uniformisation localeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9879 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-06Toujours l'unification de apply : nouveau raffinement pour ne testerherbelin
l'unification sur les types (qui nécessite le coûteux hnf_constr pour la compatibilité) que si le type contient encore des méta (et pour cela on attend le dernier moment) ou si une coercion est potentiellement à insérer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9878 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-06tail0thery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9877 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-05Gestion espaces dans notation _ = _ :> _herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9876 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-05Amélioration de la complexité de auto (l'utilisation des types dansherbelin
l'unification -r9842- avait introduit des appels inutiles et coûteux à hnf_constr). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9875 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-30Corrections dans le Print Assumption. Les definitions locales ("Let") aspiwack
sont maintenant prises en compte (ca a l'air de marcher). En plus j'ai corrige l'ordre d'impression pour que ca imprime les noms dans l'ordre alphabetique (avant c'etait l'ordre inverse, etonnament perturbant). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9873 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-30Memory optimisation for modules and constrs substitutions.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9872 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-30mul_norm for Q fixedthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9871 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-29Corrected the treatment of negative numbers for the bigZ parser. And aspiwack
corrected a small typo in an error message (bogN instead of bigN). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9870 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-29Correction d'un bug dans l'affichage du message d'erreur real_cleanherbelin
(cas d'un terme sans Rel libre), introduction au passage d'un nouveau type d'evar EvarGoal pour raffinement du message d'erreur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9868 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-28comparison functions should be Defined not Qedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9867 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-28Contrôle de la compatibilité de apply via une information dans lesherbelin
métas permettant de savoir si une instance de méta vient d'un with-binding ou d'une unification, et si elle a déjà été typée ou pas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9866 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-28Retour à un message d'erreur d'apply qui montre un échec sans sans réduction herbelin
de la conclusion du lemme git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9865 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-28Réaffichage des Structure/Record sous la forme Recordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9864 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-27As suggested by Pierre Casteran, fold for FSets/FMaps now takes a letouzey
(A:Type) instead of a (A:Set). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9863 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-25 21:51:58 +0000