aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2010-03-23Fix bug in backtracking.vgross
2010-03-23debuggingvgross
2010-03-19Removing unexpected printing of debug output (see bug report #2271).herbelin
2010-03-19Définition de GRAMMARCMA: parsing/grammar.cma n'était plus installé, ce qu...notin
2010-03-18kills a warning about vo in checker/safe_typingletouzey
2010-03-18Makefile.build: (slightly) more robust sed invocation for parsing camlp4deps/...letouzey
2010-03-18Myocamlbuild: slight simplification of code for .ml4letouzey
2010-03-15Oops, don't use zeta by default.msozeau
2010-03-15Stop dropping evar constraints when building a new goal evar defs.msozeau
2010-03-15Fix splitting evars tactics and stop dropping evar constraints whenmsozeau
2010-03-12fixed minor pbs with test casesbarras
2010-03-12fixed confusion between number of cstr arguments and number of pattern variab...barras
2010-03-11introduced lazy computation of size info in the guard conditionbarras
2010-03-11Update manual on search commandspuech
2010-03-11Minimal test suite for search commandspuech
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 08:24:07 +0000