aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* 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
| |\ \ \ | | |/ / | |/| |
| | * | [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
| |/ /
| | * Fast path for implicit tactic solving.Gravatar Pierre-Marie Pédrot2017-03-23
| |/
| * [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
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\|
* | Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Moving printing code from Evd to Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | Chasing a few unsafe constr coercions.Gravatar Pierre-Marie Pédrot2017-02-14
* | Do not ask for a normalized goal to get hypotheses and conclusions.Gravatar Pierre-Marie Pédrot2017-02-14
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Funind API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* | Quote API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14