aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2010-10-03Using multiple lists of implicit arguments in Program for preservingherbelin
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-10-03Dead code in impargs (afaics, no more need, since r11242, to mergeherbelin
2010-10-03Making display of various informations about constants more modular:herbelin
2010-10-03Fixed a little printing bug with "About" on an undefined constant.herbelin
2010-09-30Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesglondu
2010-09-30Improve handling of metas as evars in unification (patch by Hugo)letouzey
2010-09-30Speed-up refine by avoiding some calls to Evd.foldletouzey
2010-09-28Fix bug #2321, allowing "_" named projections in classes. Not realizingmsozeau
2010-09-28Coqdoc patches from UPenn (thanks to C. Casinghino). This introduces themsozeau
2010-09-28Minor fixes of 'make doc'pboutill
2010-09-28Bvector.Vshiftin was wrong for agespboutill
2010-09-28Remove some occurrences of "open Termops"glondu
2010-09-28Fix function applications without labels (OCaml warning 6)glondu
2010-09-28Remove "init" label from Termops.it_mk* specialized functionsglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 04:04:18 +0000