| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | [location] Remove Loc.ghost. |  Emilio Jesus Gallego Arias | 2017-04-25 |
| * | Merge branch 'master' into econstr |  Pierre-Marie Pédrot | 2017-04-07 |
| |\ | |||
| | * | Ensuring static invariants about handling of pending evars in Pretyping. | Pierre-Marie Pédrot | 2017-03-23 |
| * | | Merge branch 'master'. | Pierre-Marie Pédrot | 2017-02-14 |
| |\| | |||
| * | | Making Evd independent from Namegen. | 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 |
| * | | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | 2017-02-14 |
| * | | Ltac now uses evar-based constrs. | Pierre-Marie Pédrot | 2017-02-14 |
| | * | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-12-07 |
| |/| | |||
| | * | Document changes |  Matthieu Sozeau | 2016-12-02 |
| | * | Fix UGraph.check_eq! | Matthieu Sozeau | 2016-11-30 |
| * | | Reordering Termops w.r.t. Evd and Namegen in engine folder. | Pierre-Marie Pédrot | 2016-10-30 |
| |/ | |||
| * | Short documentation, filling TODO's in evd.mli. |  Hugo Herbelin | 2016-09-01 |
| * | Remove unused optional "predicative" argument. |  Guillaume Melquiond | 2016-08-10 |
| * | Univs: add source locations of levels |  Matthieu Sozeau | 2016-06-29 |
| * | Adding a bit of documentation in the mli. | Pierre-Marie Pédrot | 2016-06-09 |
| * | Allowing to attach location to universes in UState. | Pierre-Marie Pédrot | 2016-02-19 |
| * | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-02-13 |
| * | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-01-29 |
| * | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-01-21 |
| * | merge |  Matej Kosik | 2016-01-11 |
| |\ | |||
| | * | CLEANUP: kernel/context.ml{,i} | Matej Kosik | 2016-01-11 |
| * | | Remove duplicate declarations. | Guillaume Melquiond | 2016-01-01 |
| |/ | |||
| * | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-11-20 |
| * | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-11-05 |
| * | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-10-30 |
| * | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-10-29 |
| * | Clarifying and documenting the UState API. | Pierre-Marie Pédrot | 2015-10-17 |
| * | Dedicated file for universe unification context manipulation. | Pierre-Marie Pédrot | 2015-10-17 |
| * | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-10-09 |
| * | Splitting kernel universe code in two modules. | Pierre-Marie Pédrot | 2015-10-06 |
| * | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-10-02 |
| * | Removing meta_with_name from Evd. | Pierre-Marie Pédrot | 2015-09-27 |
| * | Removing subst_defined_metas_evars from Evd. | Pierre-Marie Pédrot | 2015-09-27 |
| * | Removing uselessly duplicated function in Evd. | Pierre-Marie Pédrot | 2015-09-27 |
| * | Hardening the API of evarmaps. | Pierre-Marie Pédrot | 2015-09-26 |
| * | Merge branch 'v8.5' into trunk |  Maxime Dénès | 2015-09-17 |
| * | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-06-01 |
| * | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-05-05 |
| * | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-03-23 |
| * | Adding a new folder corresponding to the low-level part of the pretyper | Pierre-Marie Pédrot | 2015-02-27 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |