aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* [pp] [ide] Minor cleanups in pp code.Gravatar Emilio Jesus Gallego Arias2017-03-21
* Remove a dead exception catching code.Gravatar Théo Zimmermann2017-03-13
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
* Adding a printer for Proof.proof reflecting the focusing layout.Gravatar Hugo Herbelin2017-01-26
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\
| * Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\|
| * Use pf_get_type_of to avoid blowup in pose proof of large proof termsGravatar Matthieu Sozeau2016-11-08
| * Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
| |\
| | * More explicit name for status of unification constraints.Gravatar Maxime Dénès2016-11-07
| * | Fix #3441 Use pf_get_type_of to avoid blowupGravatar Matthieu Sozeau2016-11-04
| | * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
| | * Unification constraint handling (#4763, #5149)Gravatar Matthieu Sozeau2016-10-22
| |/
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\|
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
| |\
| * \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
| |\ \
| | | * Merge remote-tracking branch 'git/bug5123' into v8.5Gravatar Matthieu Sozeau2016-10-12
| | |/|
| | | * Fix bug #5123: mark all shelved evars unresolvableGravatar Matthieu Sozeau2016-10-11
| | * | Fix for bug #4863, update the Proofview's env withGravatar Matthieu Sozeau2016-10-11
| | |/
| | * Fix #4416: - Incorrect "Error: Incorrect number of goals"Gravatar Arnaud Spiwack2016-10-10
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\| |
| * | Merge remote-tracking branch 'github/pr/263' into v8.6Gravatar Maxime Dénès2016-10-03
| |\ \
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\| | |
| * | | Fix bug #4723 and FIXME in API for solve_by_tacGravatar Matthieu Sozeau2016-09-28
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-27
|\| | |
| * | | Moving "move" in the new proof engine.Gravatar Hugo Herbelin2016-09-24
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\| | |
* | | | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* | | | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
| * | | Adding variants enter_one and refine_one which assume that exactly oneGravatar Hugo Herbelin2016-09-16
* | | | Make the Coq codebase independent from Ltac-related code.Gravatar Pierre-Marie Pédrot2016-09-16
|\ \ \ \
* \ \ \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\ \ \ \ \ | | |/ / / | |/| | |
| * | | | Merge remote-tracking branch 'github-coq/pr/249' into v8.6Gravatar Matthieu Sozeau2016-09-12
| |\ \ \ \
| | * | | | no-refold patchGravatar Paul Steckler2016-09-09
| * | | | | Fast path in Clenvtac.clenv_refine typeclass resolution.Gravatar Pierre-Marie Pédrot2016-09-09
| |/ / / /
| | | * / Tracking careless uses of slow name lookup.Gravatar Pierre-Marie Pédrot2016-09-09
| | |/ / | |/| |
| | * | Making Proof_global terminator generic in external tactics.Gravatar Pierre-Marie Pédrot2016-09-08
| | * | Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
| |/ / |/| |
* | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \
* \ \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\ \ \ \ | | |/ / | |/| |
| * | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-02
| |\ \ \ | | | |/ | | |/|
| | * | Fixing name of internal refine ("simple refine").Gravatar Hugo Herbelin2016-09-01
* | | | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | | | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
* | | | Merge remote-tracking branch 'v8.6' into trunkGravatar Matej Kosik2016-08-25
|\| | |
* | | | CLEANUP: Type alias "Context.section_context" was removedGravatar Matej Kosik2016-08-25
* | | | CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Gravatar Matej Kosik2016-08-25
* | | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* | | | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-24
| | | * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19