aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Sorting library: export as hints only lemmas that obviously simplifyGravatar herbelin2010-07-02
* Miscellaneous small updates:Gravatar herbelin2010-07-01
* Move [delayed] to util and use [force_delayed] everywhere to forceGravatar msozeau2010-06-30
* Fix generalize_eqs tactic to not consider defined variables as being generali...Gravatar msozeau2010-06-30
* Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.Gravatar msozeau2010-06-30
* Correct wrong handling of evars in instance definitions that preventedGravatar msozeau2010-06-29
* QArith: typo in name of hint db (fix #2346)Gravatar letouzey2010-06-29
* change the flag "internal" in declare/ind_tables from bool toGravatar vsiles2010-06-29
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* Fix compilation by replacing some "auto with zarith" with "ring"Gravatar glondu2010-06-28
* Extraction: handling modules (not functors) in Haskell by name manglingGravatar letouzey2010-06-28
* Update of documentation for the standard library (cf. #2332)Gravatar letouzey2010-06-28
* Extraction: remove a useless matchGravatar letouzey2010-06-28
* Made "replace" accepts open terms on its left-hand-side.Gravatar herbelin2010-06-28
* Fixed a bug introduced in a combination in r12807 and revealed inGravatar herbelin2010-06-28
* Applying François' patches about Canonical Projections (see #2302 and #2334).Gravatar herbelin2010-06-26
* Backporting modifications to nsatz (doc + fix of bug #2328) from trunk to v8.3.Gravatar herbelin2010-06-26
* Moved error when option does not exist into a warning (this allows toGravatar herbelin2010-06-25
* bug 2328 fixed: failure when polynomial not i idealGravatar pottier2010-06-25
* modifs de nsatz suggerees par HugoGravatar pottier2010-06-25
* Restored a "feature" of unification in pre-8.3 (it was used e.g. in aGravatar herbelin2010-06-25
* Extraction: nicer simple extraction of custom defs (fix #2204)Gravatar letouzey2010-06-23
* Names: remove obsolete mod_self_idGravatar letouzey2010-06-23
* Ajout d'une feuille de style pour les définitions spécifiques à Hevea + di...Gravatar notin2010-06-23
* Mise à jour des liens au site Coq (suite à la MAJ de la redirection DNS de ...Gravatar notin2010-06-23
* Commit 13179 continued (updated CHANGES about support for Heq's library).Gravatar herbelin2010-06-22
* Backport from trunk to 8.3 of modifications on groebner/nsatzGravatar herbelin2010-06-22
* Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).Gravatar herbelin2010-06-22
* Fixing dependencies for coqideGravatar vgross2010-06-22
* fix bug #2318, parsing error on dos line endingsGravatar vgross2010-06-22
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Protection against anomaly when loading a state with bad magic number.Gravatar herbelin2010-06-22
* Extraction: replace unicode characters in ident by ascii encodings (fix #2158...Gravatar letouzey2010-06-21
* Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)Gravatar letouzey2010-06-20
* clear/revert dependent: restrict to hyp(h) instead of ident(h)Gravatar letouzey2010-06-18
* Quick fix for having clenv debug printer working in trunk.Gravatar herbelin2010-06-18
* Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).Gravatar herbelin2010-06-18
* Documentation of clear dependent and revert dependentGravatar letouzey2010-06-18
* add in test-suite the scripts about fsetdec bugsGravatar letouzey2010-06-18
* Report fixes from FSetDecide to MSetDecideGravatar letouzey2010-06-18
* fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix #2...Gravatar letouzey2010-06-18
* fsetdec: clear dependent hypothesis before anything else (fix #2136).Gravatar letouzey2010-06-17
* New tactic "clear dependent", for the moment in ltac in Init/TacticsGravatar letouzey2010-06-17
* test for bug #2141 (include + extraction)Gravatar letouzey2010-06-16
* MSetInterface: no induction principle about a Record (nicer extraction)Gravatar letouzey2010-06-16
* Extraction: fix the eta reduction function used in code optimisationsGravatar letouzey2010-06-16
* MSetAVL: for nicer extraction, we create only tree_ind, not tree_rect and tre...Gravatar letouzey2010-06-15
* CHANGE: a word about new commands Compute and FailGravatar letouzey2010-06-15
* CHANGES: list of modifications for the extractionGravatar letouzey2010-06-15
* Extraction: in support library, more and nicer big_intGravatar letouzey2010-06-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-04 01:38:45 +0000