aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* 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
|\ \
* | | 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] 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
| * | | | Merge PR#642: Small cleanup on `close_proof` type.Gravatar Maxime Dénès2017-05-24
| |\ \ \ \ | | |/ / / | |/| | |
| | | | * Fix bindings handling of setoid_rewrite.Gravatar Cyprien Mangin2017-05-23
| | * | | [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| * | | | Change wrong bullet message.Gravatar Théo Zimmermann2017-05-20
| |/ / /
| | * | Removing unused warnings.Gravatar Pierre-Marie Pédrot2017-05-19
| | * | Generalizing the refine primitive so as to accept tactic arguments.Gravatar Pierre-Marie Pédrot2017-05-03
| |/ /
| * | Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
| |\ \
| * | | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| * | | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| * | | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| * | | Merge PR#586: trivial cleanup commits which does not change Coq APIGravatar Maxime Dénès2017-04-27
| |\ \ \
| | * | | contracting the type of "Pfedit.solve_by_implicit_tactic"Gravatar Matej Košík2017-04-27
* | | | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | | | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | | | [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
| |/ / / |/| | |
| * | | Removing the tclWEAK_PROGRESS tactical.Gravatar Pierre-Marie Pédrot2017-04-24
| * | | Removing the tclNOTSAMEGOAL primitive from the API.Gravatar Pierre-Marie Pédrot2017-04-24
|/ / /
* | | Merge PR#552: Miscelaneous commitsGravatar Maxime Dénès2017-04-24
|\ \ \
* | | | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
| * | | COMMENT: Proof_global.pstate.pidGravatar Matej Kosik2017-04-20
|/ / /
| * / Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
|/ /
* | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\ \
| * \ Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
| |\ \
* | | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\| | |
* | | | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* | | | Fix call to broken unsafe_type_of in apply tactic.Gravatar Maxime Dénès2017-03-29
* | | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\ \ \ \
| | * | | [nit] Fix a couple incorrect uses of msg_error.Gravatar Emilio Jesus Gallego Arias2017-03-24
| |/ / /