aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2015-03-08Fixing bug #2951.Pierre-Marie Pédrot
2015-03-05Do not prepend a "Error:" header when the error is expected by the user.Guillaume Melquiond
2015-02-27Fixing OCaml 3.12 compilation.Pierre-Marie Pédrot
2015-02-27Fixing bug #3249.Pierre-Marie Pédrot
2015-02-24Univs: Fix Check calling the kernel to retype in the wrong environment.Matthieu Sozeau
2015-02-19Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Pierre-Marie Pédrot
2015-02-18Fix bug #4046.Matthieu Sozeau
2015-02-17Remove Whelp commands.Maxime Dénès
2015-02-16Fix bug #3960: potential evar instance categorized as an unresolvableMatthieu Sozeau
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-02-13Better error message for nested module application.Maxime Dénès
2015-02-12Fix typos about .vio files (thanks Arthur for spotting them)Enrico Tassi
2015-02-12Revert "Using same code for browsing physical directories in coqtop and coqdep."Hugo Herbelin
2015-02-12Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Hugo Herbelin
2015-02-12Capital letter in plugins.Hugo Herbelin
2015-02-12Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
2015-02-11Tactic Notation: use stable unique key for notations (Close: 3970)Enrico Tassi
2015-02-10Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ...Hugo Herbelin
2015-02-05Properly set module names in presence of -Q. (Fix for bug #3958)Guillaume Melquiond
2015-02-04Optimized Import/Export the same way as Require Import/Export wasHugo Herbelin
2015-02-04Tactic Notation: use stable unique key for notations (Close: 3970)Enrico Tassi
2015-02-03Revert "Tactic Notation: use stable unique key for notations (Close: 3970)"Enrico Tassi
2015-02-03Tactic Notation: use stable unique key for notations (Close: 3970)Enrico Tassi
2015-02-03spit module path using / as directory separatorEnrico Tassi
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-29Prevent spurious warnings about Arguments.Guillaume Melquiond
2015-01-24Equality Schemes options: reverting commit ff9f94634 which isHugo Herbelin
2015-01-24Isolate a function for printing evar sets.Hugo Herbelin
2015-01-21Add the possibility of defining opaque terms with program.mlasson
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-17Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-15Make -print-mod-uid accept a list of files.Maxime Dénès
2015-01-13Made -print-mod-uid more silent and robust.Maxime Dénès
2015-01-12Add -no-native-compiler flag to list dumped by --help.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2015-01-11Avoiding a redundant information in unification error message.Hugo Herbelin
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2015-01-06rename: vi -> vioEnrico Tassi
2015-01-06Fix some documentation typos.Guillaume Melquiond
2015-01-05kernel/ind Change interface of declare_mind and declare_mutualMatthieu Sozeau
2015-01-05In Show Universes, print universes before normalization.Matthieu Sozeau
2014-12-29Fixing bug #3632 for good.Pierre-Marie Pédrot
2014-12-29Proof using: do not clear letins (unless they use a cleared var)Enrico Tassi
2014-12-28Proof using: call "clear" to remove from sight the vars not selectedEnrico Tassi
2014-12-28remove debug prints (leftover)Enrico Tassi
2014-12-19Better doc and a few fixes for Proof using.Enrico Tassi
2014-12-18Proof using: New vernacular to name sets of section variablesEnrico Tassi
2014-12-17STM: rename and simplify flagsEnrico Tassi
2014-12-17Arguments: warn only if no option is given (Close 3860)Enrico Tassi
2014-12-16Fixing CAMLP4 compilation.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 21:45:53 +0000