aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-11-21New Arguments vernaculargareuselesinge
2011-11-21Configurable simpl tacticgareuselesinge
2011-11-21coqide default pref files are by default in /etc/xdg/coq/pboutill
2011-11-21/home/pirbo/.coqrc* are read againpboutill
2011-11-21-user option removalpboutill
2011-11-21Updated CHANGES file wrt to pattern-matching compilation.herbelin
2011-11-21Extend the computation of dependencies in pattern-matching compilationherbelin
2011-11-21Add matching on non-inductive types in building an inversion problemherbelin
2011-11-21Old naming bug in pattern-matching compilation: names in theherbelin
2011-11-21Inlining let-in (i.e. trace of aliases) in extract_predicate for whatherbelin
2011-11-21VectorDef.v takes benefit of dependencies being taken into accountherbelin
2011-11-21In pattern-matching compilation, now taking into account the dependenciesherbelin
2011-11-21Optimizing the compilation of unused aliases in pattern-matching.herbelin
2011-11-21Simplifying history management in pattern-matching compilation.herbelin
2011-11-21Fixing postprocessing bugs in pattern-matching compilation.herbelin
2011-11-21Removing stuff about alias dependencies now become useless.herbelin
2011-11-21Changed the way to detect if an "as" patterns is expanded or not. Theherbelin
2011-11-21Updating Cases.v test.herbelin
2011-11-21Dead code + refreshing some comments in cases.ml.herbelin
2011-11-21Typoherbelin
2011-11-20CHANGES updatepboutill
2011-11-20coqrc in the right XDG_CONFIG_HOME/coq folderpboutill
2011-11-20coqide-gtk2rc not dottedpboutill
2011-11-20CoqIdE configuration file won't pollute your home anymorepboutill
2011-11-20Teach coq_makefile how to install into XDG_DATA_HOME.pboutill
2011-11-20Add support for XDG_DATA_HOME and XDG_DATA_DIRS.pboutill
2011-11-20coq_makefile: Don't install with +x.pboutill
2011-11-20coq_makefile: Add Makefile variables specifying installpboutill
2011-11-18Adding the type infrastructure to handle properly API management of optionsppedrot
2011-11-18Fix parsing of :>> and backtrack correctly on the cache of hints for local co...msozeau
2011-11-18Return of the tactic hints features in CoqIDE.ppedrot
2011-11-18Added hint support in the API. You can now query a goal to see the tactics th...ppedrot
2011-11-18Toplevel loop is a bit more robust: it catches bad API queries.ppedrot
2011-11-18Making status info better in CoqIDE: path and name of current lemmappedrot
2011-11-18Now Coqtop has a richer way to answer a query about its pending goals. Answer...ppedrot
2011-11-18Added a printing function to handle single evarsppedrot
2011-11-18Replaced goal api call with a proper structure. This disables menu hints in C...ppedrot
2011-11-18Coqide -debug only printed Coqtop information.pboutill
2011-11-18Restore backward compatibility. ":>" declares subinstances in Class declarati...msozeau
2011-11-18Fix for subclasses implementation, allowing to register generalized classes s...msozeau
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
2011-11-17Fixing new bug introduced in r14665 when fixing bug #1834.herbelin
2011-11-17Merge fix for bug #2604.msozeau
2011-11-17Fix bug #2604, wrong error from setoid_rewrite. The rewrite is impossible due...msozeau
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-11-17Was missing a potential application of subtypingmsozeau
2011-11-16Adding postprocessing to remove "commutative cuts" expansions inherbelin
2011-11-16Changed the way find_dependencies_signature is working so that itherbelin
2011-11-16De Bruijn indices bug in pattern matching compilation in the presenceherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 16:26:11 +0000