aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inGravatar letouzey2008-06-01
* BigQ: starting to create and use an interface QSigGravatar letouzey2008-06-01
* Enhance the BigN and BigZ infrastructure: Gravatar letouzey2008-06-01
* Improve the dependent induction tactic to automatically find theGravatar msozeau2008-05-30
* NBigN: proofs that BigN implements axioms of NAxiomsSigGravatar letouzey2008-05-29
* - Modification de la déf de minus et pred conformément aux remarques deGravatar herbelin2008-05-28
* Notation concise pour la valeur par défaut des cas reconnus commeGravatar herbelin2008-05-28
* Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are Gravatar letouzey2008-05-28
* CyclicAxioms: after discussion with Laurent, znz_WW and variants areGravatar letouzey2008-05-28
* - Correction bug highlighting "Module" dans CoqideGravatar herbelin2008-05-28
* Cyclic31: proofs for addmuldiv31, tail031 and head031. Only two Admitted left !Gravatar letouzey2008-05-28
* Cyclic31: proof of auxiliary function iter_int31 + (failed) attempt at provin...Gravatar letouzey2008-05-27
* Correction du problème de complexité de Print Assumptions :Gravatar aspiwack2008-05-27
* Cyclic31: migrate auxiliary lemmas to their legitimate filesGravatar letouzey2008-05-27
* Cyclic31 : proof of the spec of gcd31Gravatar letouzey2008-05-27
* Int31 : gcd31 was wrongGravatar letouzey2008-05-26
* Cyclic31: cleanup, 2 Admitted killed (6 remaining)Gravatar letouzey2008-05-26
* Cyclic31 : replace the ugly time-consuming brute-force proof by a reasonable ...Gravatar letouzey2008-05-23
* (Not completely finished) proofs that int31 integers fulfill the CyclicAxioms...Gravatar letouzey2008-05-23
* writing a match on a digit via syntax "if ... then ... else" is not a good id...Gravatar letouzey2008-05-22
* Proposition for a almost-bitsize-independent Int31.v (joint work with J. Voui...Gravatar letouzey2008-05-22
* QRewrite is now obsolete. It was containing manual ltac stuffGravatar letouzey2008-05-22
* switch theories/Numbers from Set to Type (both the abstract and the bignum pa...Gravatar letouzey2008-05-22
* Minor improvement: group stuff about carry apart from stuff about zn2zGravatar letouzey2008-05-19
* Thanks to Matthieu's commit 10941, Ad-hoc tactics contained in QRewrite are n...Gravatar letouzey2008-05-19
* ZModulo: Z viewed modulo 2^digits implements CyclicAxiomsGravatar letouzey2008-05-17
* Fix a de Bruijn bug in setoid_rewrite when rewriting underGravatar msozeau2008-05-17
* Filename ZnZ (or Z_nZ in a later attempt) is neither pretty nor accurateGravatar letouzey2008-05-16
* BigNum: more reorganization, mainly moves GenXYZ to DoubleXYZGravatar letouzey2008-05-16
* ZTreeMod was meant to prove that BigZ correspond to the Integer Axioms.Gravatar letouzey2008-05-16
* More BigNum cleanup: Gravatar letouzey2008-05-16
* In practice, the new setoid rewrite (and the "at" syntax) allows to avoid Gravatar letouzey2008-05-15
* Coq headers + $ in theories/Numbers filesGravatar letouzey2008-05-15
* Various fixes:Gravatar msozeau2008-05-15
* MAJ et bricoles diversesGravatar herbelin2008-05-12
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* - Changement du code de Zplus pour accomoder ring qui sinon prend uneGravatar herbelin2008-05-11
* Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]Gravatar herbelin2008-05-09
* remove mention of an obsolete limitation of Add MorphismGravatar letouzey2008-05-08
* Oups, my new version of NMake_gen.ml was relying on a 3.10 feature:Gravatar letouzey2008-05-08
* Integration of theories/Ints into theories/Numbers, again : better generation...Gravatar letouzey2008-05-08
* Integration of theories/Ints into theories/Numbers, part 3: auto-generation o...Gravatar letouzey2008-05-08
* Integration of theories/Ints into theories/Numbers, part 1: moving filesGravatar letouzey2008-05-07
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* Backtrack commit 10887 (priorité des notations pour les signatures deGravatar notin2008-05-05
* It seems more natural to put those operators at same level as "->"...Gravatar glondu2008-05-05
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laGravatar herbelin2008-04-29
* Fix eauto still using delta when it shouldn't (should make CoRN compileGravatar msozeau2008-04-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 16:28:46 +0000