aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* change into QuestionMark defaultGravatar Siddharth Bhat2018-07-17
* Change QuestionMark for better record field missing error message.Gravatar Siddharth Bhat2018-07-17
* Merge PR #7983: Turn a dead branch into an assertion failure in VM reification.Gravatar Maxime Dénès2018-07-10
|\
* \ Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument.Gravatar Matthieu Sozeau2018-07-09
|\ \
| | * Turn a dead branch into an assertion failure in VM reification.Gravatar Pierre-Marie Pédrot2018-07-05
| |/ |/|
* | Merge PR #7746: Many small cleanups removing unused arguments and functionsGravatar Pierre-Marie Pédrot2018-07-05
|\ \
| * | Glob_ops.rename_glob_vars: fix typoGravatar Gaëtan Gilbert2018-07-03
| * | Glob_ops.fix_kind_eq: fix typoGravatar Gaëtan Gilbert2018-07-03
| * | Remove unused env argument to fresh_sort_in_familyGravatar Gaëtan Gilbert2018-07-03
* | | Merge PR #7607: Simplify reification of predicate in bytecode and native comp...Gravatar Pierre-Marie Pédrot2018-07-03
|\ \ \ | |/ / |/| |
* | | Merge PR #7080: Swapping Context and Constr and defining declarations on cons...Gravatar Maxime Dénès2018-06-29
|\ \ \
* | | | Deprecate Environ.retroknowledge function in favor of the projectionGravatar Gaëtan Gilbert2018-06-28
| | * | Simplify reification of predicate in bytecode and native compilersGravatar Maxime Dénès2018-06-28
| |/ / |/| |
* | | Merge PR #7866: Implementation of mutual records in the higher strataGravatar Maxime Dénès2018-06-28
|\ \ \
| | * | Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
| |/ / |/| |
* | | Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
| * | Handle mutual records in upper layers.Gravatar Pierre-Marie Pédrot2018-06-24
|/ /
* | Merge PR #7827: [engine] safe [add_unification_pb] interfaceGravatar Pierre-Marie Pédrot2018-06-23
|\ \
* | | Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
* | | Change the proj_ind field from MutInd.t to inductive.Gravatar Pierre-Marie Pédrot2018-06-23
| | * Fix #5719: Uncaught exception Invalid_argument.Gravatar Pierre-Marie Pédrot2018-06-21
* | | Rename Dyn.TParam→ValueS, Dyn.MapS.obj→value to clarify their purpose.Gravatar whitequark2018-06-21
| |/ |/|
* | Merge PR #7797: Remove reference name type.Gravatar Enrico Tassi2018-06-19
|\ \
* \ \ Merge PR #6754: Better elaboration of pattern-matchings on primitive projectionsGravatar Pierre-Marie Pédrot2018-06-19
|\ \ \
* \ \ \ Merge PR #7801: [vernac] Add option to force building really mutual induction...Gravatar Enrico Tassi2018-06-19
|\ \ \ \
* \ \ \ \ Merge PR #7714: Remove primitive-projection related data from the kernelGravatar Maxime Dénès2018-06-19
|\ \ \ \ \
| | | | * | Remove reference name type.Gravatar Maxime Dénès2018-06-18
| |_|_|/ / |/| | | |
| * | | | Remove the proj_body field from the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
| * | | | Remove the proj_eta field of the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
* | | | | Fixes #7811 (uncaught Not_found in notation printer related to "match").Gravatar Hugo Herbelin2018-06-17
|/ / / /
| | * / Better elaboration of pattern-matchings on primitive projectionsGravatar Matthieu Sozeau2018-06-15
| |/ / |/| |
| | * evd/evarutil: safe [add_unification_pb] interface, taking EConstr'sGravatar Matthieu Sozeau2018-06-15
| |/ |/|
* | Fix deprecation warning introduced by PR 664 mergeGravatar Matthieu Sozeau2018-06-14
* | Merge PR #664: Fixing #5500 (missing test in return clause of match leading t...Gravatar Matthieu Sozeau2018-06-14
|\ \
* \ \ Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder i...Gravatar Matthieu Sozeau2018-06-14
|\ \ \
* \ \ \ Merge PR #7105: Getting rid of some false "collision between bound variable n...Gravatar Matthieu Sozeau2018-06-14
|\ \ \ \
| | | | * [vernac] Add option to force building really mutual induction schemesGravatar Matthieu Sozeau2018-06-13
| |_|_|/ |/| | |
* | | | [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
* | | | [api] Misctypes removal: tactic flags.Gravatar Emilio Jesus Gallego Arias2018-06-12
* | | | [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* | | | [api] Misctypes removal: remove dummy alias.Gravatar Emilio Jesus Gallego Arias2018-06-12
* | | | [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | * | Fixes #7780 (missing lift in expanding alias under a binder in unification).Gravatar Hugo Herbelin2018-06-12
| |/ / |/| |
* | | Merge PR #7679: Clean native compilation of primitive projectionsGravatar Maxime Dénès2018-06-05
|\ \ \
* \ \ \ Merge PR #7004: Make `simple apply` obey `Opaque` directive.Gravatar Pierre-Marie Pédrot2018-06-05
|\ \ \ \
* \ \ \ \ Merge PR #7077: Preserving canonical structure of return predicate in vm_comp...Gravatar Maxime Dénès2018-06-05
|\ \ \ \ \
| | | * | | More straightforward native compilation of primitive projections.Gravatar Pierre-Marie Pédrot2018-06-05
| |_|/ / / |/| | | |
* | | | | Merge PR #7099: Stronger invariants in unification signature.Gravatar Matthieu Sozeau2018-06-05
|\ \ \ \ \
| | | * | | Make direct invocations of `simple apply` obey `Opaque` directive.Gravatar Maxime Dénès2018-06-05
| |_|/ / / |/| | | |
| | * | | Preserving "canonical" form of return predicate in native_compute.Gravatar Hugo Herbelin2018-06-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 10:52:19 +0000