aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2010-04-13Remove only *.v.log files in clean of test-suite/Makefileglondu
2010-04-11Look for csdp in $PATH at runtime, remove -csdpdir configure optionglondu
2010-04-11Remove unused functions run_sdpaglondu
2010-04-11Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").herbelin
2010-04-10Run parallelized test-suite in "check" target of main Makefileglondu
2010-04-10Prettier test-suite/Makefileglondu
2010-04-10Optimized need for delimiters when disjoint scopes for strings andherbelin
2010-04-10Update .gitignoreglondu
2010-04-10Use the Makefile in test-suite/checkglondu
2010-04-10Makefile for the test-suiteglondu
2010-04-10Fix typos in test-suite scriptglondu
2010-04-10Granting wish #2229 (InA_dec transparent) and Michael Day's coq-clubherbelin
2010-04-10Test for bug #2231 (unexpected error when using let/if over an inductiveherbelin
2010-04-10Partially fixed bug #2231 (an inductive parameter name was internallyherbelin
2010-04-10Fixing various coqdep bugs (#2118, #2242, #2274)herbelin
2010-04-09Change definition of FSetList so that equality is Leibnizglondu
2010-04-09Add test-suite/lia.cache to .gitignoreglondu
2010-04-09Fixing part 1 of bug #2242 (-I -as and -R -as were supported forherbelin
2010-04-09Granting wish #2249 (checking existing lemma name also when in a section).herbelin
2010-04-09Documenting the use of ##, %%, $$ in coqdoc.herbelin
2010-04-09Applied Cédric Auger's patch to fix use of "#&xxx;" in html printingherbelin
2010-04-07Commit 12906 continued (forgotten file).herbelin
2010-04-07Granting wish #2251 thanks to commit 12900 solved bug 1416.v (whichherbelin
2010-04-06New model for user-driven translation of tokens in coqdocherbelin
2010-04-05Improving compatibility between 8.2 and 8.3herbelin
2010-04-05Fix configure script: natdynlink works without a hack on 10.6.3.msozeau
2010-04-05Added a function in typing.ml to solve evars of a constr w/o going back down ...herbelin
2010-04-05Changement de ide/proofs.ml en ide/ideproofs.ml pour éviter un conflitaspiwack
2010-04-05Granting wish #2251 (forbidding rewriting a term reduced to an evar)herbelin
2010-04-05Tests for bug report #2244 (pattern-unification with abstraction over Meta's)herbelin
2010-04-05Partial fix to bug #2244 (ensure that pattern unification does notherbelin
2010-03-31Add documentation on the treatment of [if] and [let (x1, ... xn) := ..]msozeau
2010-03-30Small things about coqdoc + fixing lettuple.v test (part of bug #2289)herbelin
2010-03-30Removed hard-wiring of latin1 letters in coqdoc (see bug #2275)herbelin
2010-03-30Small improvements around coqdoc (including fix for bug #2288)herbelin
2010-03-30Fixed small bugs introduced in commit 12890 (bug #2286, that comesherbelin
2010-03-30Manual qualification of Mfourier.Proof in micromega to avoid ocamldep using i...letouzey
2010-03-30Improving error messages in the presence of utf-8 charactersherbelin
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2010-03-28Extended on-the-fly eta-expansion in coercion mechanism to sort-polymorphicherbelin
2010-03-28Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt)herbelin
2010-03-27Fixing bug #2279 (printing nested let-in was in exponential time)herbelin
2010-03-27Applied greenrd's patch to fix bug 2255 (injection failed toherbelin
2010-03-24Fixed bug #2260 (check of resolution of all evars in the declarationherbelin
2010-03-23Updated CHANGES wrt 8.3herbelin
2010-03-23Added automatic expansion on the left of recursive notationsherbelin
2010-03-23Changing types to reflect futur separation between toplevel and ide.vgross
2010-03-23infrastructure for safe marshal-based IPCvgross
2010-03-23Goal generation deported into ide/coq.ml, single function to obtainvgross
2010-03-23New functions for goals fetching.vgross
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 06:48:34 +0000