aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* [vernac] Remove "Proof using" hacks from parser.Gravatar Emilio Jesus Gallego Arias2017-10-10
* Take Suggest Proof Using outside the kernel.Gravatar Gaëtan Gilbert2017-10-10
* Merge PR #1109: Handle some misc todosGravatar Maxime Dénès2017-10-09
|\
| * Cleanup suggest_bulletGravatar Gaëtan Gilbert2017-09-29
* | Efficient computation of the names contained in an environment.Gravatar Pierre-Marie Pédrot2017-09-28
* | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
|/
* proof_global: cleanup and comment close_proofGravatar Matthieu Sozeau2017-09-19
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* Fix a refine anomaly "Evar defined twice".Gravatar Pierre-Marie Pédrot2017-09-06
* Merge PR #946: Functional pretyping interfaceGravatar Maxime Dénès2017-08-29
|\
* \ Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\ \
| | * Move glob_constr_ltac_closure to evar_refiner.Gravatar Maxime Dénès2017-08-01
| |/ |/|
* | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \
| * | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* | | Statically ensuring that inlined entries out of the kernel have no effects.Gravatar Pierre-Marie Pédrot2017-07-26
* | | More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
|/ /
* | [api] Put modules in order in API.{mli,ml}Gravatar Emilio Jesus Gallego Arias2017-07-25
* | Merge PR #899: [general] Move files to directories so they match linking order.Gravatar Maxime Dénès2017-07-20
|\ \
* \ \ Merge PR #770: [proof] Move bullets to their own module.Gravatar Maxime Dénès2017-07-19
|\ \ \
| | * | [general] Move files to directories matching linking order.Gravatar Emilio Jesus Gallego Arias2017-07-19
| |/ / |/| |
* | | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| | * Moving "assert" (internally "Cut") to the new proof engine.Gravatar Hugo Herbelin2017-06-25
| | * Exporting general-purpose functions on goal contexts from "logic.ml" to "tact...Gravatar Hugo Herbelin2017-06-25
| |/ |/|
* | Merge PR#777: Improving documentation of tactic "move" (report #4561)Gravatar Maxime Dénès2017-06-19
|\ \
* | | Remove Warnings: unused value ...Gravatar Amin Timany2017-06-16
* | | Squashed commit of the following:Gravatar Amin Timany2017-06-16
* | | Merge PR#763: [proof] Deprecate redundant wrappers.Gravatar Maxime Dénès2017-06-14
|\ \ \
* \ \ \ Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \ \ \
| | | * | Improving documentation of tactic "move" (report #4561).Gravatar Hugo Herbelin2017-06-13
* | | | | Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
* | | | | Turn the default behaviour of the refine primitive into the safe one.Gravatar Pierre-Marie Pédrot2017-06-13
| |_|/ / |/| | |
| | | * [proof] Move bullets to their own module.Gravatar Emilio Jesus Gallego Arias2017-06-12
| |_|/ |/| |
| | * [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
| |/ |/|
| * A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\
* \ Merge PR#717: [proof] Deprecate "proof mode" APIGravatar Maxime Dénès2017-06-07
|\ \
* | | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* | | Don't double up on periods in anomaliesGravatar Jason Gross2017-06-02
* | | Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Maxime Dénès2017-06-02
|\ \ \
| * | | [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
* | | | Merge PR#696: Trunk+cleanup constr of globalGravatar Maxime Dénès2017-06-01
|\ \ \ \
| | | * | [proof] Deprecate "proof mode" APIGravatar Emilio Jesus Gallego Arias2017-05-31
| | |/ /
* | / / Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
| |/ / |/| |
| * | Cleanup: removal of constr_of_global.Gravatar Matthieu Sozeau2017-05-29
|/ /
* | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\ \
* \ \ Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \ \
* \ \ \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \ \
| | * | | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24