aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2010-07-02Extraction: better support of modulesletouzey
2010-07-02Extraction: no more MPself hence no need for subst during ppletouzey
2010-07-02Remove dependency to Unix from module Profileglondu
2010-07-02Sorting library: export as hints only lemmas that obviously simplifyherbelin
2010-07-01Miscellaneous small updates:herbelin
2010-06-30Move [delayed] to util and use [force_delayed] everywhere to forcemsozeau
2010-06-30Fix generalize_eqs tactic to not consider defined variables as being generali...msozeau
2010-06-30Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.msozeau
2010-06-29Correct wrong handling of evars in instance definitions that preventedmsozeau
2010-06-29QArith: typo in name of hint db (fix #2346)letouzey
2010-06-29change the flag "internal" in declare/ind_tables from bool tovsiles
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-06-28Fix compilation by replacing some "auto with zarith" with "ring"glondu
2010-06-28Extraction: handling modules (not functors) in Haskell by name manglingletouzey
2010-06-28Update of documentation for the standard library (cf. #2332)letouzey
2010-06-28Extraction: remove a useless matchletouzey
2010-06-28Made "replace" accepts open terms on its left-hand-side.herbelin
2010-06-28Fixed a bug introduced in a combination in r12807 and revealed inherbelin
2010-06-26Applying François' patches about Canonical Projections (see #2302 and #2334).herbelin
2010-06-26Backporting modifications to nsatz (doc + fix of bug #2328) from trunk to v8.3.herbelin
2010-06-25Moved error when option does not exist into a warning (this allows toherbelin
2010-06-25bug 2328 fixed: failure when polynomial not i idealpottier
2010-06-25modifs de nsatz suggerees par Hugopottier
2010-06-25Restored a "feature" of unification in pre-8.3 (it was used e.g. in aherbelin
2010-06-23Extraction: nicer simple extraction of custom defs (fix #2204)letouzey
2010-06-23Names: remove obsolete mod_self_idletouzey
2010-06-23Ajout d'une feuille de style pour les définitions spécifiques à Hevea + di...notin
2010-06-23Mise à jour des liens au site Coq (suite à la MAJ de la redirection DNS de ...notin
2010-06-22Commit 13179 continued (updated CHANGES about support for Heq's library).herbelin
2010-06-22Backport from trunk to 8.3 of modifications on groebner/nsatzherbelin
2010-06-22Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).herbelin
2010-06-22Fixing dependencies for coqidevgross
2010-06-22fix bug #2318, parsing error on dos line endingsvgross
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-22Protection against anomaly when loading a state with bad magic number.herbelin
2010-06-21Extraction: replace unicode characters in ident by ascii encodings (fix #2158...letouzey
2010-06-20Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)letouzey
2010-06-18clear/revert dependent: restrict to hyp(h) instead of ident(h)letouzey
2010-06-18Quick fix for having clenv debug printer working in trunk.herbelin
2010-06-18Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).herbelin
2010-06-18Documentation of clear dependent and revert dependentletouzey
2010-06-18add in test-suite the scripts about fsetdec bugsletouzey
2010-06-18Report fixes from FSetDecide to MSetDecideletouzey
2010-06-18fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix #2...letouzey
2010-06-17fsetdec: clear dependent hypothesis before anything else (fix #2136).letouzey
2010-06-17New tactic "clear dependent", for the moment in ltac in Init/Tacticsletouzey
2010-06-16test for bug #2141 (include + extraction)letouzey
2010-06-16MSetInterface: no induction principle about a Record (nicer extraction)letouzey
2010-06-16Extraction: fix the eta reduction function used in code optimisationsletouzey
2010-06-15MSetAVL: for nicer extraction, we create only tree_ind, not tree_rect and tre...letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 21:38:32 +0000