aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2010-09-28Remove kind_of_type, kind_of_term2 (dead code)glondu
2010-09-27Fix bug in implementation of setoid rewriting under cases andmsozeau
2010-09-24Fixed a bug in printing fix/cofix error messages when severalherbelin
2010-09-24Solving bug #2212 (unification under tuples now not allowed forherbelin
2010-09-24Partial review of removed dead code (r13460)herbelin
2010-09-24Checker: remove some dead codeletouzey
2010-09-24Dead code in extractionletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-24dev/Makefile.oug: how to run the Oug analyser, for instance for finding dead ...letouzey
2010-09-23Added a section in the documentation of Vernacular commands about Set/Unset/T...aspiwack
2010-09-23Update CHANGES: Local/Global Set/Unset.aspiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 08:39:51 +0000