aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2007-11-15Split NTimesOrder into properly NTimesOrder and NPlusOrder.emakarov
2007-11-14Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder...emakarov
2007-11-13Correcting a segfault on amd64 arch with native compiler of ocaml 3.10jforest
2007-11-12Correction du bug #1741notin
2007-11-10A result about Zsgn(a/b), both for Zdiv and ZOdivletouzey
2007-11-10First reasonably complete version of ZOdiv, including some propertiesletouzey
2007-11-09Nettoyage de Print Assumptions :aspiwack
2007-11-09Suite ajout raccourcis à compute et lazy pour réduire tout saufherbelin
2007-11-09git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10309 85f007b7-540e-0...jforest
2007-11-09Rétablissement compatibilité constr_of_referenceherbelin
2007-11-09more about ZOdiv and ZOmod (still not finished)letouzey
2007-11-08Corrected the ML code for well-founded recursion in the comment.emakarov
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
2007-11-08Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.emakarov
2007-11-08setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. letouzey
2007-11-08small copy&paste bug in zify: some Pmult should be Nmultletouzey
2007-11-07git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10300 85f007b7-540e-0...emakarov
2007-11-07Forgot a backslash in Makefile.common. Added "(only parsing)" in BinNat.v.emakarov
2007-11-07Replaced BinNat with a new version that is based on theories/Numbers/Natural/...emakarov
2007-11-07bug in infos_and_sort: type of constructor was not reduced enoughbarras
2007-11-06small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is letouzey
2007-11-06bugs dpfilliatr
2007-11-06Oups. Clflags.recursive_types isnt normally accessible on a standard ocaml in...letouzey
2007-11-06Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...letouzey
2007-11-06useless Require Export Extractionletouzey
2007-11-05For debugging with coqtop.byte with ocaml 3.10, the toplevel should be made w...letouzey
2007-11-05Suppress from the ouputs of SearchAbout all lemmas generated by "abstract"letouzey
2007-11-04Fix bug#1739msozeau
2007-11-03An update of theories/Numbersemakarov
2007-11-01two additionnal results on list append (coming from theories/ints/List/ListAu...letouzey
2007-11-01A way to specialize universally quantified hypothesis: if H is letouzey
2007-11-01Adding Qround.v (and helper lemmas and hints)roconnor
2007-11-01In agreement with Laurent Thery, start migration of auxiliary results letouzey
2007-10-30temporary workaround for bug #1738letouzey
2007-10-30A useless Add Morphism: since Subset is a Setoid Relation, it is alsoletouzey
2007-10-30bug in safe_typing: univ constraints generated by section variables were not ...barras
2007-10-30Changement esthétique de la preuve de mult_is_onenotin
2007-10-30Ajout de lemmes d'inversion pour mult (sur le modèle de plus_is_O et plus_is...notin
2007-10-30Cleaning code and comment.courtieu
2007-10-29Revision of the FSetWeak Interface, so that it becomes a precise letouzey
2007-10-29Amélioration du message d'erreur dans end_module, end_module_type et close_s...notin
2007-10-29MAJherbelin
2007-10-27Réparation d'une inefficacité bêtement introduite dans la révisionherbelin
2007-10-25small fix of commit 10188: a string given via Extract Inductive can be emptyletouzey
2007-10-25Adding BigQ and proofsthery
2007-10-25Added NIso.v to Makefile.common. Changed Examples.v in contrib/micromega to u...emakarov
2007-10-24Quelques exemples à méditer sur le polymorphisme d'universe des inductifsherbelin
2007-10-24Fix define body bug fixmsozeau
2007-10-24Fix define body bugmsozeau
2007-10-24Addition of more general tactics for equality. Functional extensionality and ...msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 15:23:15 +0000