aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Fix a normalization hotspot in computation of constr keys.Gravatar Pierre-Marie Pédrot2017-04-06
* Removing a normalization hotspot from EConstr.Gravatar Pierre-Marie Pédrot2017-04-05
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\
* | 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
* | Revert to incorrect heuristic in apply.Gravatar Maxime Dénès2017-03-28
* | Fix interpretation of Ltac patterns episode 2.Gravatar Maxime Dénès2017-03-24
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\ \
| | * Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| |/
| * Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
| |\
| | * Intern names bound in match patternsGravatar Tej Chajed2017-03-23
| * | Merge PR#437: Improve unification debug trace.Gravatar Maxime Dénès2017-03-17
| |\ \
* | | | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\| | |
* | | | Quick hack to fix interpretation of patterns in Ltac.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Dedicated datatype for aliases in Evarsolve.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Putting back the occur_meta_or_undefined_evar function in the old term API.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
* | | | Putting back the subst_defined_metas_evars function in the old term API.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
* | | | Cleaning up interfaces.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Removing compatibility layers related to printing.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
* | | | Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Cc API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Reductionops 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
* | | | Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Class_tactics 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
* | | | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Cleaning up opening of the EConstr module in pretyping folder.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
* | | | Coercion API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Classops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Typeclasses API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 07:33:50 +0000