aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2007-07-11dead codeletouzey
2007-07-11Slight cleanup of refl_omega.ml : in particular it uses now listletouzey
2007-07-11Added ForAll_Str_nth_tlroconnor
2007-07-10Big reorganization of romega/ReflOmegaCore.v: towards a modular letouzey
2007-07-09Petites corrections sur le Makefilenotin
2007-07-09More natural notation for intro pattern: @a -> ?aglondu
2007-07-09Improvements / Bug fixes for ROmega letouzey
2007-07-07If a fixpoint is not written with an explicit { struct ... }, then letouzey
2007-07-06a few works about my commits since Februaryletouzey
2007-07-06minor bug correction (continuing r 9943)jforest
2007-07-06Update of theories/Numbers directory.emakarov
2007-07-06Adding a syntax for "n-ary" rewrite: letouzey
2007-07-06sequel to commit 9952: forgot to adapt xlate to the new n-ary renameletouzey
2007-07-06extension of the rename tactic: the following is now allowed: letouzey
2007-07-06Documentation for commit 9774.glondu
2007-07-06New intro pattern "@A", which generates a fresh name based on A.glondu
2007-07-06Documentation related to commit 9948: intropattern {A,B,C} for (A,(B,C))letouzey
2007-07-06Suggestion of additional syntax for intro patterns: letouzey
2007-07-05Update on numbers.emakarov
2007-07-05Added Qpower_mult theorem.roconnor
2007-07-05documentation of f_equal and revert and case_eq (and s/lri.fr/pps.jussieu.fr/...letouzey
2007-07-05Minor bug correction in Function. Non terminating Function e.g. jforest
2007-07-03Compatibilité des noms longs de Bool déplacés dans Datatypesherbelin
2007-07-02Correction (partielle) du bug #1587notin
2007-07-02Missing include path of ocaml .h when generating depsmsozeau
2007-07-02Better handling of aliases, add command to solve a particular obligation.msozeau
2007-07-02Fix bug in subst_cases_pattern when aliasing recursive notations.msozeau
2007-07-02Factorisation des paramètres dans l'affichage des inductifsherbelin
2007-06-30Correction bug sur factorisation affichage paramètres (cf r9918)herbelin
2007-06-30Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Recordherbelin
2007-06-30- Ajout de la possibilité d'utiliser la notation Record pour lesherbelin
2007-06-29Added the directory theories/Numbers where axiomatizations and implementation...emakarov
2007-06-27- Extensions of FMap(Weak)Facts: letouzey
2007-06-27eqlistA is now equivlistAletouzey
2007-06-26killing some more non-exhaustive patternsletouzey
2007-06-26kill an ugly warning about a non-exhaustive patternletouzey
2007-06-26Oups: thanks to ./configure -reals no, I was not building the whole dependenc...letouzey
2007-06-26Added zwqipWith.roconnor
2007-06-26additional properties for FMap (and slight rework of SetoidList and FSetPrope...letouzey
2007-06-25Updated Qpow_tac to work on a a more realistic set of exponent values.roconnor
2007-06-22Ajout exist & cie à la table des hints par symétrie avec ex_intro &herbelin
2007-06-21Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc, notin
2007-06-21Simplification de la construction du .depend:notin
2007-06-21Correction de plusieurs bugs de l'export XML (utilisation d'un type deherbelin
2007-06-21Adding: Field instance for Q.roconnor
2007-06-20ajout de head0 et tail0 en natifbgregoir
2007-06-19safe_shift correct recursionthery
2007-06-19safe_shift recursionthery
2007-06-19safe_shift recursionthery
2007-06-19typo faqherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 00:43:25 +0000