Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | | | Remove some unused values and types | Gaetan Gilbert | 2017-04-27 | |
| * | | | Fix omitted labels in function calls | Gaetan Gilbert | 2017-04-27 | |
| * | | | Merge PR#586: trivial cleanup commits which does not change Coq API | Maxime Dénès | 2017-04-27 | |
| |\ \ \ | ||||
| | * | | | contracting the type of "Pfedit.solve_by_implicit_tactic" | Matej Košík | 2017-04-27 | |
* | | | | | [location] Make location optional in Loc.located | Emilio Jesus Gallego Arias | 2017-04-25 | |
* | | | | | [location] Remove Loc.ghost. | Emilio Jesus Gallego Arias | 2017-04-25 | |
* | | | | | [location] Use located in misctypes. | Emilio Jesus Gallego Arias | 2017-04-24 | |
| |/ / / |/| | | | ||||
| * | | | Removing the tclWEAK_PROGRESS tactical. | Pierre-Marie Pédrot | 2017-04-24 | |
| * | | | Removing the tclNOTSAMEGOAL primitive from the API. | Pierre-Marie Pédrot | 2017-04-24 | |
|/ / / | ||||
* | | | Merge PR#552: Miscelaneous commits | Maxime Dénès | 2017-04-24 | |
|\ \ \ | ||||
* | | | | Remove VernacError | Gaetan Gilbert | 2017-04-21 | |
| * | | | COMMENT: Proof_global.pstate.pid | Matej Kosik | 2017-04-20 | |
|/ / / | ||||
| * / | Update various comments to use "template polymorphism" | Gaetan Gilbert | 2017-04-11 | |
|/ / | ||||
* | | Merge branch 'master' into econstr | Pierre-Marie Pédrot | 2017-04-07 | |
|\ \ | ||||
| * \ | Merge PR#508: Optimize pending evars | Maxime Dénès | 2017-04-06 | |
| |\ \ | ||||
* | | | | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-04-04 | |
|\| | | | ||||
* | | | | Using delayed universe instances in EConstr. | Pierre-Marie Pédrot | 2017-04-01 | |
* | | | | Fix call to broken unsafe_type_of in apply tactic. | Maxime Dénès | 2017-03-29 | |
* | | | | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-03-24 | |
|\ \ \ \ | ||||
| | * | | | [nit] Fix a couple incorrect uses of msg_error. | Emilio Jesus Gallego Arias | 2017-03-24 | |
| |/ / / | ||||
| | * / | Fast path for implicit tactic solving. | Pierre-Marie Pédrot | 2017-03-23 | |
| |/ / | ||||
| * | | [pp] [ide] Minor cleanups in pp code. | Emilio Jesus Gallego Arias | 2017-03-21 | |
| * | | Remove a dead exception catching code. | Théo Zimmermann | 2017-03-13 | |
| * | | [stm] Break stm/toplevel dependency loop. | Emilio Jesus Gallego Arias | 2017-02-15 | |
* | | | Merge branch 'master'. | Pierre-Marie Pédrot | 2017-02-14 | |
|\| | | ||||
* | | | Removing most nf_enter in tactics. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Namegen primitives now apply on evar constrs. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Moving printing code from Evd to Termops. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Chasing a few unsafe constr coercions. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Do not ask for a normalized goal to get hypotheses and conclusions. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Definining EConstr-based contexts. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Introducing contexts parameterized by the inner term type. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Evar-normalizing functions now act on EConstrs. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Funind API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Ltac now uses evar-based constrs. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Removing compatibility layers in Retyping | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Quote API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Reductionops now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Proofview.Goal primitive now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Eliminating parts of the right-hand side compatibility layer | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Rewrite API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Eqdecide API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Hints API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Tacticals API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Clenv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Tacmach API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Refine API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Goal API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |