aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Merge remote-tracking branch 'github/pr/223' into feedback-locationsGravatar Maxime Dénès2016-06-27
|\
* | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| * [feedback] Add optional ?loc parameter to loggers.Gravatar Emilio Jesus Gallego Arias2016-06-25
|/
* Merge remote-tracking branch 'github/pr/212' into trunkGravatar Maxime Dénès2016-06-20
|\
| * Add file name, line number and beginning of line position to locations.Gravatar Maxime Dénès2016-06-20
* | Fix bug #4836: Anomaly: Uncaught exception Invalid_argument.Gravatar Pierre-Marie Pédrot2016-06-19
* | Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
* | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* | Print the type-in-type flag in various user-facing functions.Gravatar Pierre-Marie Pédrot2016-06-18
|/
* Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
* Protect the beautifier from change in the lexer state (typically byGravatar Hugo Herbelin2016-06-16
* Merge '/pr/206' into trunkGravatar Enrico Tassi2016-06-16
|\
* \ Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
* | | --print-version produces machine readable version infoGravatar Enrico Tassi2016-06-16
* | | Merge remote-tracking branch 'github/pr/194' into trunkGravatar Maxime Dénès2016-06-16
|\ \ \
| | * | Remove the syntax changes introduced by this branch.Gravatar Pierre-Marie Pédrot2016-06-15
| | * | Allow `Pretyping.search_guard` to not check guardGravatar Arnaud Spiwack2016-06-15
| | * | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | | | Preventive compatibility fixes for flushing.Gravatar Emilio Jesus Gallego Arias2016-06-14
* | | | Fix for bug #4784Gravatar Emilio Jesus Gallego Arias2016-06-14
| | | * Allow catching of EvaluatedError exceptions.Gravatar Emilio Jesus Gallego Arias2016-06-14
| |_|/ |/| |
* | | Merge remote-tracking branch 'origin/pr/166' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \
* \ \ \ Merge remote-tracking branch 'origin/pr/182' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ \
* \ \ \ \ Merge remote-tracking branch 'origin/pr/173' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ \ \
* \ \ \ \ \ Merge branch "LtacProf for trunk" (PR #165).Gravatar Pierre-Marie Pédrot2016-06-14
|\ \ \ \ \ \
| * | | | | | Moving back Ltac profiling to the Ltac folder.Gravatar Pierre-Marie Pédrot2016-06-14
* | | | | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-13
|\ \ \ \ \ \ \
| * | | | | | | Tentatively fixing misguiding error message with "binder" type inGravatar Hugo Herbelin2016-06-13
| * | | | | | | Reserve exception "ConversionFailed" in unification for failure ofGravatar Hugo Herbelin2016-06-12
| * | | | | | | Fixing bug in printing CannotSolveConstraint (collision of context names).Gravatar Hugo Herbelin2016-06-12
* | | | | | | | Search interface revisions.Gravatar Pierre-Marie Pédrot2016-06-07
|\ \ \ \ \ \ \ \
| * | | | | | | | Removing the convenience functions from the Search API.Gravatar Pierre-Marie Pédrot2016-06-07
| | | | | | | * | Adding an only printing flag to notations.Gravatar Pierre-Marie Pédrot2016-06-07
| | | | | | | * | Removing the use to Egramcoq.recover_constr_grammar.Gravatar Pierre-Marie Pédrot2016-06-07
| |_|_|_|_|_|/ / |/| | | | | | |
| | | | * | | | STM: each proof block can be enabled separatelyGravatar Enrico Tassi2016-06-06
| | | | * | | | STM: proof block detection made optional + simple testGravatar Enrico Tassi2016-06-06
| |_|_|/ / / / |/| | | | | |
| | * | | | | Fixing problems introduced in 8.5 with Ltac trace report. E.g.Gravatar Hugo Herbelin2016-06-06
| | | * | | | -profileltac -> -profile-ltac, as per @herbelinGravatar Jason Gross2016-06-05
| | | * | | | LtacProf for Coq trunkGravatar Jason Gross2016-06-05
| |_|/ / / / |/| | | | |
* | | | | | coqtop: Add ltac/ to search path.Gravatar Matthieu Sozeau2016-06-02
| | | * | | STM delegation policy can be customizedGravatar Enrico Tassi2016-05-31
| | * | | | Revert "Rename Lexer -> CLexer."Gravatar Pierre-Marie Pédrot2016-05-31
* | | | | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| |_|/ / / |/| | | |
| | | * | fix blanks in usage messageGravatar Enrico Tassi2016-05-19
| | | * | coqc: support -o option to specify output file nameGravatar Enrico Tassi2016-05-19
| |_|/ / |/| | |
* | | | Put the "exact_constr" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | | Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\ \ \ \ | | |/ / | |/| |
| * | | Fix bug #3887: Better error message for "More than one program with unsolved ...Gravatar Pierre-Marie Pédrot2016-05-09
| * | | Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09