aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
| | * | | | | Documenting "Set Structural Injection".Gravatar Hugo Herbelin2016-08-21
| | * | | | | Do not recompute the whole evar naming environment in GProd intepretation.Gravatar Pierre-Marie Pédrot2016-08-21
| | * | | | | Short path for Pretyping.ltac_interp_name_env.Gravatar Pierre-Marie Pédrot2016-08-21
* | | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-08-21
|\ \ \ \ \ \ \ | | |/ / / / / | |/| | | | |
| * | | | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-21
| |\ \ \ \ \ \ | | | |_|_|/ / | | |/| | | |
| * | | | | | More standard naming for the Imparg.with_implicits function.Gravatar Pierre-Marie Pédrot2016-08-20
| * | | | | | Fixing a bug in the presence of let-in while inferring the return clause.Gravatar Hugo Herbelin2016-08-20
| | * | | | | Fixing an anomaly in printing a unification error message.Gravatar Hugo Herbelin2016-08-20
| * | | | | | Test file for bug #4187.Gravatar Pierre-Marie Pédrot2016-08-19
| * | | | | | Fix performance bug: do not compute implicits of abstracted lemmas.Gravatar Pierre-Marie Pédrot2016-08-19
| * | | | | | Removing dead code in Impargs.Gravatar Pierre-Marie Pédrot2016-08-19
| | | | | * | [pp] Fix bug 4842 (Time prints in multiple lines)Gravatar Emilio Jesus Gallego Arias2016-08-19
| * | | | | | Merge remote-tracking branch 'origin/pr/246' into v8.6Gravatar Matthieu Sozeau2016-08-19
| |\ \ \ \ \ \
| * | | | | | | Moving Taccoerce to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-08-19
| | | * | | | | Remove extraneous dot in error message (bug #4832).Gravatar Guillaume Melquiond2016-08-19
| * | | | | | | Fix anomaly on user-inputted projection name (bug #5029).Gravatar Guillaume Melquiond2016-08-19
| | |_|_|_|/ / | |/| | | | |
| | | | | | * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
| |_|_|_|_|/ |/| | | | |
| | | | | * [pp] Fix newline issues.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | |_|_|/ | |/| | |
| * | | | Merge remote-tracking branch 'github/bug4978' into v8.6Gravatar Matthieu Sozeau2016-08-18
| |\ \ \ \
| * \ \ \ \ Merge remote-tracking branch 'github/bug4188' into v8.6Gravatar Matthieu Sozeau2016-08-18
| |\ \ \ \ \
| | | | | * | Fix incorrect glob data for module symbols (bug #2336).Gravatar Guillaume Melquiond2016-08-18
| * | | | | | Fix an occurrence of deprecated eqn syntax in stdlib.Gravatar Maxime Dénès2016-08-18
| * | | | | | Fix bug #4939: LtacProf prints tactic notations weirdly.Gravatar Pierre-Marie Pédrot2016-08-18
| * | | | | | Adding a test for bug #4653.Gravatar Pierre-Marie Pédrot2016-08-18
| * | | | | | Merge PR #256 into v8.6Gravatar Pierre-Marie Pédrot2016-08-18
| |\ \ \ \ \ \
| | * | | | | | In docs, fix command to reset Ltac profilingGravatar Paul Steckler2016-08-17
| |/ / / / / /
| | * | | | | Fix setoid_rewrite to raise proper errorsGravatar Matthieu Sozeau2016-08-17
| | | | | * | Fixing #5001 (metas not cleaned properly in clenv_refine_in).Gravatar Hugo Herbelin2016-08-17
| | | | | * | Fixing CHANGES.Gravatar Hugo Herbelin2016-08-17
| * | | | | | Documenting fix of #3070 (subst and chain of dependencies).Gravatar Hugo Herbelin2016-08-17
| |/ / / / /
* | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-08-17
|\| | | | |
* | | | | | Revert "CLEANUP: removing the definition of the "Context.Rel.Declaration.to_t...Gravatar Pierre-Marie Pédrot2016-08-17
| |_|_|_|/ |/| | | |
| | * | | Fix #4978: priorities of Equivalence instancesGravatar Matthieu Sozeau2016-08-17
| |/ / /
| * | | Fixing #3070 ("subst" taking properly into account chains of dependencies).Gravatar Hugo Herbelin2016-08-17
| * | | Two protections against failures when printing evar_map.Gravatar Hugo Herbelin2016-08-17
| * | | Fixing printing in debugger (no global env in debugger).Gravatar Hugo Herbelin2016-08-17
| * | | A fix to dev/include.Gravatar Hugo Herbelin2016-08-17
| | | * infoH: output via msg_* to make the XML protocol happyGravatar Enrico Tassi2016-08-17
| * | | Removing dead unsafe debugging code in Constrintern.Gravatar Pierre-Marie Pédrot2016-08-16
| | | * Output a break before a list only if there was an empty line (bug #4606).Gravatar Guillaume Melquiond2016-08-16
| * | | Merge PR #250 into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
| |\ \ \
| * \ \ \ Merge PR #237 into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
| |\ \ \ \
| * \ \ \ \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
| |\ \ \ \ \ | | | |_|_|/ | | |/| | |
| * | | | | Efficiently generate the pretyping contexts.Gravatar Pierre-Marie Pédrot2016-08-16
| |\ \ \ \ \
| | | * \ \ \ Merge branch 'pr255' into v8.5 (bug #5015)Gravatar Guillaume Melquiond2016-08-16
| | | |\ \ \ \
| | | | * | | | Fix regression in Coqide's "forward one command" commandGravatar Xavier Leroy2016-08-14
| | | |/ / / /
* | | | | | | Adding "Context.Named.Declaraton.of_rel" functionGravatar Matej Kosik2016-08-11
* | | | | | | CLEANUP: removing the definition of the "Context.Rel.Declaration.of_tuple" fu...Gravatar Matej Kosik2016-08-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 00:08:29 +0000