aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Merge PR#379: Introducing evar-insensitive constrsGravatar Maxime Dénès2017-04-11
|\
* | Revert "refactoring: Reductionops.contextual_reduction_function type"Gravatar Matej Košík2017-04-10
* | refactoring: Reductionops.contextual_reduction_function typeGravatar Matej Kosik2017-04-10
| * Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
| |\
* | | Turning the printing primitive projection parameter flag off by default.Gravatar Hugo Herbelin2017-04-07
* | | Turning the printing primitive projection compatibility flag off by default.Gravatar Hugo Herbelin2017-04-07
| |/ |/|
* | Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
|\ \
| | * 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
| |_|/ |/| |
| * | Better algorithm for Evarconv.max_undefined_with_candidates.Gravatar Pierre-Marie Pédrot2017-03-24
* | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
|\ \ \
| * | | Intern names bound in match patternsGravatar Tej Chajed2017-03-23
| | * | Make the computation of frozen evars lazy in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| | * | Fast path in computation of frozen evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| | * | Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 06:54:22 +0000