aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* 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 #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
* | 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
* | 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
| | * | | Preserving "canonical" form of return predicate in vm_compute.Gravatar Hugo Herbelin2018-06-04
| |/ / / |/| | |
* | | | Merge PR #7199: Fixes #7195: missing freshness condition in Ltac pattern-matc...Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \
* \ \ \ \ Merge PR #7189: Fix #5539: algebraic universe produced by cases.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \
| | | * | | Stronger invariants in unification signature.Gravatar Pierre-Marie Pédrot2018-06-04
| |_|/ / / |/| | | |
* | | | | Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ta...Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7216: Replace uses of Termops.dependent by more specific functions.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7234: Reduce circular dependency constants <-> projectionsGravatar Maxime Dénès2018-06-01
|\ \ \ \ \ \ \ \
* | | | | | | | | [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31