aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Expand)AuthorAge
* Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
* [pp] Remove uses of expensive string_of_ppcmds.Gravatar Emilio Jesus Gallego Arias2017-03-21
* Proofview: tclINDEPENDENTLGravatar Enrico Tassi2017-02-10
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
|\
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-01-23
* | Adding a new evar source to remember the name of evars which wereGravatar Hugo Herbelin2017-01-22
* | Merge remote-tracking branch 'github/pr/350' into trunkGravatar Maxime Dénès2017-01-09
|\ \
* \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|\ \ \ | | |/ | |/|
| * | Document changesGravatar Matthieu Sozeau2016-12-02
| * | Fix UGraph.check_eq!Gravatar Matthieu Sozeau2016-11-30
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\| |
| | * tclDISPATCH: more informative error messageGravatar Arnaud Spiwack2016-11-08
| |/ |/|
| * Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
| |\
| | * Fixes to compile with ocaml 4.01Gravatar Matthieu Sozeau2016-11-07
| * | Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ \ | | |/ | |/|
* | | Moving unused code out of the kernel into Termops.Gravatar Pierre-Marie Pédrot2016-10-31
* | | Stronger static invariant in equality upto universes.Gravatar Pierre-Marie Pédrot2016-10-31
* | | Code factorization in Universes.Gravatar Pierre-Marie Pédrot2016-10-31
* | | Moving Universes to the engine/ folder.Gravatar Pierre-Marie Pédrot2016-10-30
* | | Reordering Termops w.r.t. Evd and Namegen in engine folder.Gravatar Pierre-Marie Pédrot2016-10-30
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\| |
| * | Merge remote-tracking branch 'github/pr/321' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ \
| * | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
* | | | COMMENT: Namegen.next_ident_awayGravatar Matej Kosik2016-10-26
* | | | COMMENT: Proofview.entryGravatar Matej Kosik2016-10-26
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| | |
| | | * Unification constraint handling (#4763, #5149)Gravatar Matthieu Sozeau2016-10-22
| | |/ | |/|
| * | Oops, my bad, didn't expect a merge issue!Gravatar Matthieu Sozeau2016-10-21
| * | Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-10-21
| | * sections/hints: prevent Not_found in get_type_ofGravatar Matthieu Sozeau2016-10-21
| |/
* | CLEANUP: Namegen.to_avoidGravatar Matej Kosik2016-10-20
* | CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\|
| * Fix bug #5145: Anomaly: index to an anonymous variable.Gravatar Pierre-Marie Pédrot2016-10-15
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\|
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\|
| * Merge remote-tracking branch 'github/pr/263' into v8.6Gravatar Maxime Dénès2016-10-03
| |\
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\| |
| * | Adding variants enter_one and refine_one which assume that exactly oneGravatar Hugo Herbelin2016-09-16
| | * Tracking careless uses of slow name lookup.Gravatar Pierre-Marie Pédrot2016-09-09
| |/
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-07
|\ \ \ | | |/ | |/|
| * | Fast path in push_rel_context_to_named_context.Gravatar Pierre-Marie Pédrot2016-09-05
| * | Fast path in whd_evar.Gravatar Pierre-Marie Pédrot2016-09-02
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\| |
| * | Short documentation, filling TODO's in evd.mli.Gravatar Hugo Herbelin2016-09-01
* | | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30