aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Adding the tactic "instantiate" (without argument), to force theGravatar glondu2007-12-07
* Ocaml toplevel convenience.Gravatar glondu2007-12-07
* Util.option_compare devient Option.Misc.Compare et change un peu de type Gravatar aspiwack2007-12-07
* Petit oubli de thery.Gravatar glondu2007-12-07
* Adding MemoFunction + Lowering HeightGravatar thery2007-12-06
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Commit intermédiaire express de réparation de coqide.ml, que j'avais Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Ajout de l'axiomatisation des entiers à la documentation de la librairie sta...Gravatar notin2007-11-28
* bug correction in functional inversion principle generationGravatar jforest2007-11-27
* minor bug correction in FunctionGravatar jforest2007-11-26
* * A few Parameter Inline, but they dont seem to help much concerning Gravatar letouzey2007-11-24
* small improvements about Qc. Beware: Qlt_trans becomes Qclt_trans (as it ough...Gravatar letouzey2007-11-24
* An update on Numbers. Added two files dealing with recursion, for information...Gravatar emakarov2007-11-22
* Extraction inlines Wf.Fix by default (wish of Y.Bertot)Gravatar letouzey2007-11-21
* extensible versionGravatar thery2007-11-21
* Bug in functionnal induction principle generationGravatar jforest2007-11-19
* Added theorems; created NZPlusOrder from NTimesOrder.Gravatar emakarov2007-11-16
* Split NTimesOrder into properly NTimesOrder and NPlusOrder.Gravatar emakarov2007-11-15
* Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder...Gravatar emakarov2007-11-14
* Correcting a segfault on amd64 arch with native compiler of ocaml 3.10Gravatar jforest2007-11-13
* Correction du bug #1741Gravatar notin2007-11-12
* A result about Zsgn(a/b), both for Zdiv and ZOdivGravatar letouzey2007-11-10
* First reasonably complete version of ZOdiv, including some propertiesGravatar letouzey2007-11-10
* Nettoyage de Print Assumptions :Gravatar aspiwack2007-11-09
* Suite ajout raccourcis à compute et lazy pour réduire tout saufGravatar herbelin2007-11-09
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10309 85f007b7-540e-0...Gravatar jforest2007-11-09
* Rétablissement compatibilité constr_of_referenceGravatar herbelin2007-11-09
* more about ZOdiv and ZOmod (still not finished)Gravatar letouzey2007-11-09
* Corrected the ML code for well-founded recursion in the comment.Gravatar emakarov2007-11-08
* Prise en compte des notations "alias" dans la globalisation des coercions.Gravatar herbelin2007-11-08
* Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.Gravatar emakarov2007-11-08
* setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. Gravatar letouzey2007-11-08
* small copy&paste bug in zify: some Pmult should be NmultGravatar letouzey2007-11-08
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10300 85f007b7-540e-0...Gravatar emakarov2007-11-07
* Forgot a backslash in Makefile.common. Added "(only parsing)" in BinNat.v.Gravatar emakarov2007-11-07
* Replaced BinNat with a new version that is based on theories/Numbers/Natural/...Gravatar emakarov2007-11-07
* bug in infos_and_sort: type of constructor was not reduced enoughGravatar barras2007-11-07
* small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is Gravatar letouzey2007-11-06
* bugs dpGravatar filliatr2007-11-06
* Oups. Clflags.recursive_types isnt normally accessible on a standard ocaml in...Gravatar letouzey2007-11-06
* Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...Gravatar letouzey2007-11-06
* useless Require Export ExtractionGravatar letouzey2007-11-06
* For debugging with coqtop.byte with ocaml 3.10, the toplevel should be made w...Gravatar letouzey2007-11-05
* Suppress from the ouputs of SearchAbout all lemmas generated by "abstract"Gravatar letouzey2007-11-05
* Fix bug#1739Gravatar msozeau2007-11-04
* An update of theories/NumbersGravatar emakarov2007-11-03
* two additionnal results on list append (coming from theories/ints/List/ListAu...Gravatar letouzey2007-11-01
* A way to specialize universally quantified hypothesis: if H is Gravatar letouzey2007-11-01
* Adding Qround.v (and helper lemmas and hints)Gravatar roconnor2007-11-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 19:41:39 +0000