aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Expand)AuthorAge
* [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* "tclENV" is sexier, use it instead of "Env.get"Gravatar Matej Kosik2017-04-20
* reduce syntactic noiseGravatar Matej Kosik2017-04-20
* Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\
* | Restore a fast path in EConstr instance normalization.Gravatar Pierre-Marie Pédrot2017-04-01
* | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* | Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
* | Make the Constr.kind_of_term type parametric in sorts and universes.Gravatar Pierre-Marie Pédrot2017-03-31
* | Ensuring proper cast invariants in EConstr.kind.Gravatar Pierre-Marie Pédrot2017-03-31
* | Revert "Specially crafted EConstr.kind to be more efficient."Gravatar Pierre-Marie Pédrot2017-03-31
* | Specially crafted EConstr.kind to be more efficient.Gravatar Pierre-Marie Pédrot2017-03-30
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\ \
| | * 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
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\|
* | Missing API in EConstr.Gravatar Enrico Tassi2017-02-14
* | Moving evar-normalization functions to EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Making Evd independent from Namegen.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
* | 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
* | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
* | Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Leminv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Inv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Contradiction API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Hipattern API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tacticals API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Refine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Cases API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Typeclasses API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 10:31:57 +0000