aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2010-10-23Automatically translate hints of the form "c _ ... _" into "c". Besidesherbelin
2010-10-23Fixing bug #2412 (preprocessing of Ltac Debug errors forgotten in r13431).herbelin
2010-10-22FMapFacts: typo noticed by Aaronletouzey
2010-10-22Still another Open Scope than should be Localletouzey
2010-10-21Solve name conflict about pow introduced by commit 13546.letouzey
2010-10-21Still some more Cpow in Type rather than Set (cf. r13542)letouzey
2010-10-20Oups, new file Zsqrt_def was exporting Z_scopeletouzey
2010-10-19Numbers: no need for advanced functions (e.g. sqrt) in NStrongRec, NDefOps, etcletouzey
2010-10-19Add sqrt in Numbersletouzey
2010-10-17About "unsupported" unicode characters in notations.herbelin
2010-10-16Fix missing -coqlib argument to coqdep in test-suiteglondu
2010-10-16Support for GNU Make 3.82glondu
2010-10-14Numbers : also axiomatize constants 1 and 2.letouzey
2010-10-14Reparation du parseur/printer de nombres BigNletouzey
2010-10-14Numbers: new functions pow, even, odd + many reorganisationsletouzey
2010-10-14Zeven: some complements, e.g. proofs that Zeven_bool and co are okletouzey
2010-10-14NArith: add some functions Neven and Noddletouzey
2010-10-14NArith: Definition of a Npow power functionletouzey
2010-10-14Ring : Cpow in Type rather than Set (type of power coeffs in power_theory)letouzey
2010-10-12Adding test-case for bug #2362, which uses HO unification duringmsozeau
2010-10-12Fix bug #2393: allow let-ins inside telescopes (only fails when there'smsozeau
2010-10-11Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, loopingherbelin
2010-10-11More precise description of boolean ring in doc (see bug #2401)glondu
2010-10-08Export the "bullet" grammar entryglondu
2010-10-08update CHANGES w.r.t. extractionletouzey
2010-10-07Fix bug# 2392msozeau
2010-10-07TeX input method is now supported upstreamvgross
2010-10-07test-suite: fix success/unification.vglondu
2010-10-06Fixing the Not_found error in bug #2404 + dead code removal in cases.mlherbelin
2010-10-06Remove Explain* vernacsglondu
2010-10-06Extraction: allow to use Extraction Inline / NoInline even from under a section.letouzey
2010-10-06test-suite: fix output/Existentials.outglondu
2010-10-06Remove ide/coq_tactics.ml*glondu
2010-10-06Remove VernacGoglondu
2010-10-06Remove unused unshare_proof_tree from xml pluginglondu
2010-10-06Remove open_subgoals field of proof_treeglondu
2010-10-05(Hopefully) clearer explanation of Ltac's context patternsglondu
2010-10-05test-suite: fix success/Typeclasses.vglondu
2010-10-05test-suite: fix success/AdvancedCanonicalStructure.vglondu
2010-10-05Export definition of type implicits_list for contribs + fixed aherbelin
2010-10-05Reintroduce kind_of_type (used by Presburger contrib)glondu
2010-10-05Auto-inlining of f_terminate in Functionjforest
2010-10-05test-suite: use unified diff output and use expected output as referenceglondu
2010-10-04Forgotten lifts in eta-expansionglondu
2010-10-04Install a printer for fconstr (ppconstr was installed twice)glondu
2010-10-04Two [Evd.fold] turned into [Evd.fold_undefined].aspiwack
2010-10-04Fixing bugs in previous commits about implicit arguments:herbelin
2010-10-03Avoid raising an anomaly when an error encapsulated with a dummyherbelin
2010-10-03Test for non-regression of the display bug fixed in r13486.herbelin
2010-10-03Fixing printing of module_path names (was using a debuggingherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 02:54:41 +0000