aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2015-02-27Adding a new folder corresponding to the low-level part of the pretyperPierre-Marie Pédrot
2015-02-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-24Univs: Fix Check calling the kernel to retype in the wrong environment.Matthieu Sozeau
2015-02-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-19Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Pierre-Marie Pédrot
2015-02-18Merge branch 'v8.5'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-16Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
2015-02-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
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-11Merge branch 'v8.5'Pierre-Marie Pédrot
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-10Merge branch 'v8.5'Pierre-Marie Pédrot
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-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-01-29Prevent spurious warnings about Arguments.Guillaume Melquiond
2015-01-25Merge branch 'v8.5' into trunk.Pierre-Marie Pédrot
2015-01-24Equality Schemes options: reverting commit ff9f94634 which isHugo Herbelin
2015-01-24Isolate a function for printing evar sets.Hugo Herbelin
2015-01-23Merge branch 'v8.5' into trunkMaxime Dénès
2015-01-21Add the possibility of defining opaque terms with program.mlasson
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
2015-01-18Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-18Make native compiler handle universe polymorphic definitions.Maxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-10 09:56:17 +0000