aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* Better error message for nested module application.Gravatar Maxime Dénès2015-02-13
* Fix typos about .vio files (thanks Arthur for spotting them)Gravatar Enrico Tassi2015-02-12
* Revert "Using same code for browsing physical directories in coqtop and coqdep."Gravatar Hugo Herbelin2015-02-12
* Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Gravatar Hugo Herbelin2015-02-12
* Capital letter in plugins.Gravatar Hugo Herbelin2015-02-12
* Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-12
* Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-11
* Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ...Gravatar Hugo Herbelin2015-02-10
* Properly set module names in presence of -Q. (Fix for bug #3958)Gravatar Guillaume Melquiond2015-02-05
* Optimized Import/Export the same way as Require Import/Export wasGravatar Hugo Herbelin2015-02-04
* Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-04
* Revert "Tactic Notation: use stable unique key for notations (Close: 3970)"Gravatar Enrico Tassi2015-02-03
* Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-03
* spit module path using / as directory separatorGravatar Enrico Tassi2015-02-03
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Prevent spurious warnings about Arguments.Gravatar Guillaume Melquiond2015-01-29
* Equality Schemes options: reverting commit ff9f94634 which isGravatar Hugo Herbelin2015-01-24
* Isolate a function for printing evar sets.Gravatar Hugo Herbelin2015-01-24
* Add the possibility of defining opaque terms with program.Gravatar mlasson2015-01-21
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
* Make -print-mod-uid accept a list of files.Gravatar Maxime Dénès2015-01-15
* Made -print-mod-uid more silent and robust.Gravatar Maxime Dénès2015-01-13
* Add -no-native-compiler flag to list dumped by --help.Gravatar Maxime Dénès2015-01-12
* Update headers.Gravatar Maxime Dénès2015-01-12
* Avoiding a redundant information in unification error message.Gravatar Hugo Herbelin2015-01-11
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-06
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
* In Show Universes, print universes before normalization.Gravatar Matthieu Sozeau2015-01-05
* Fixing bug #3632 for good.Gravatar Pierre-Marie Pédrot2014-12-29
* Proof using: do not clear letins (unless they use a cleared var)Gravatar Enrico Tassi2014-12-29
* Proof using: call "clear" to remove from sight the vars not selectedGravatar Enrico Tassi2014-12-28
* remove debug prints (leftover)Gravatar Enrico Tassi2014-12-28
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* STM: rename and simplify flagsGravatar Enrico Tassi2014-12-17
* Arguments: warn only if no option is given (Close 3860)Gravatar Enrico Tassi2014-12-17
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Error messages of Searchxxx are coherent with goal selector.Gravatar Pierre Courtieu2014-12-16
* Failing on unbound notation variable in notation level modifiersGravatar Hugo Herbelin2014-12-15
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
* Util.un_op -> Option.defaultGravatar Pierre Boutillier2014-12-14
* Searchxxx now interpret patterns in goal environment if any.Gravatar Pierre Courtieu2014-12-12
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
* Added a CannotSolveConstraint unification error and made experimentsGravatar Hugo Herbelin2014-12-11
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 17:37:07 +0000