aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
Commit message (Expand)AuthorAge
* A refined solution to the beta-iota discrepancies between 8.4 and 8.5 "refine".Gravatar Hugo Herbelin2017-04-27
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\
| * Fixing #5460 (limitation in computing deps in pattern-matching compilation).Gravatar Hugo Herbelin2017-04-08
* | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\ \
* | | Namegen primitives now apply on evar constrs.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
* | | Removing various compatibility layers of tactics.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
* | | 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
* | | Leminv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Tactics 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
* | | 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
* | | Typing 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
* | | Evardefine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
| |\|
| * | Adding a new evar source to remember the name of evars which wereGravatar Hugo Herbelin2017-01-22
| | * Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).Gravatar Hugo Herbelin2017-01-22
| * | 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-10-29
|\|
| * Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).Gravatar Hugo Herbelin2016-10-29
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\|
| * Attempt to improve error rendering in pattern-matching compilation (#5142).Gravatar Hugo Herbelin2016-10-19
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\|
| * Completing reverting generalization and cleaning of the return clause inference.Gravatar Hugo Herbelin2016-10-13
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\|
| * Reverting generalization and cleaning of the return clause inference in v8.6.Gravatar Hugo Herbelin2016-10-11
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\|
| * Quick fix to #4595 (making notations containing "ltac:" unused for printing).Gravatar Hugo Herbelin2016-10-04
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-27
|\|
| * Posssible abstractions over goal variables when inferring match return clause.Gravatar Hugo Herbelin2016-09-26
| * Trying an abstracting dependencies heuristic for the match return clause even...Gravatar Hugo Herbelin2016-09-26
| * Trying a no-inversion no-dependency heuristic for match return clause.Gravatar Hugo Herbelin2016-09-26
| * Inference of return clause: giving uniformly priority to "small inversion".Gravatar Hugo Herbelin2016-09-26
* | Propagate location info on pattern match compilation.Gravatar Emilio Jesus Gallego Arias2016-09-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 04:32:10 +0000