aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
Commit message (Expand)AuthorAge
* 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é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
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| |/ |/|
* | Fixing a bug in the presence of let-in while inferring the return clause.Gravatar Hugo Herbelin2016-08-20
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* Disallow dependent case on prim records w/o etaGravatar Matthieu Sozeau2016-07-06
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Program: cleanup in cases, add optionsGravatar Matthieu Sozeau2016-06-29
* Rework treatment of default transparency of obligationsGravatar Matthieu Sozeau2016-06-27
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-02
|\
* | Revert "Add support for generalization also on named variables in pattern-mat...Gravatar Hugo Herbelin2016-04-27
* | Revert "Add support for deep dependencies in variables within the recursive s...Gravatar Hugo Herbelin2016-04-27
* | Revert "Fixing a De Bruijn bug in computing return predicate by inversion."Gravatar Hugo Herbelin2016-04-27
* | Revert "Using existing names as a basis for the inner names of the pattern-ma...Gravatar Hugo Herbelin2016-04-27
* | Revert "Vers un filtrage profond ..."Gravatar Hugo Herbelin2016-04-27
* | Vers un filtrage profond ...Gravatar Hugo Herbelin2016-04-27
* | Using existing names as a basis for the inner names of the pattern-matching p...Gravatar Hugo Herbelin2016-04-27
* | Fixing a De Bruijn bug in computing return predicate by inversion.Gravatar Hugo Herbelin2016-04-27
* | Add support for deep dependencies in variables within the recursive structure.Gravatar Hugo Herbelin2016-04-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 17:44:26 +0000