aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* Merge PR #7080: Swapping Context and Constr and defining declarations on ↵Gravatar Maxime Dénès2018-06-29
|\ | | | | | | constr in Constr
* | 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
| |/ |/| | | | | | | | | | | | | | | This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate).
* | 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
| | | | | | | | | | This brings more compatibility with handling of mutual primitive records in the kernel.
* | Change the proj_ind field from MutInd.t to inductive.Gravatar Pierre-Marie Pédrot2018-06-23
| | | | | | | | | | This is a first step towards the acceptance of mutual record types in the kernel.
* | 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 ↵Gravatar Enrico Tassi2018-06-19
|\ \ \ \ | | | | | | | | | | | | | | | induction schemes
* \ \ \ \ 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
| |_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
| * | | | Remove the proj_body field from the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was completely wrong, such a term could not even be type-checked by the kernel as it was internally using a match construct over a negative record. They were luckily only used in upper layers, namley printing and extraction. Recomputing the projection body might be costly in detyping, but this only happens when the compatibility flag is turned on, which is not the default. Such flag is probably bound to disappear anyways. Extraction should be fixed though so as to define directly primitive projections, similarly to what has been done in native compute.
| * | | | Remove the proj_eta field of the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This field was not used inside the kernel and not used in performance-critical code where caching is essential, so we extrude the code that computes it out of the kernel.
* | | | | 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
| |/ / |/| | | | | | | | | | | This ensures that computations are shared as much as possible, mimicking the "positive" records computational behavior if possible.
| | * evd/evarutil: safe [add_unification_pb] interface, taking EConstr'sGravatar Matthieu Sozeau2018-06-15
| |/ |/| | | | | Avoid adding the same unification problem twice, module evar instantiation.
* | 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 ↵Gravatar Matthieu Sozeau2018-06-14
|\ \ | | | | | | | | | to anomaly)
* \ \ Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder ↵Gravatar Matthieu Sozeau2018-06-14
|\ \ \ | | | | | | | | | | | | in unification
* \ \ \ Merge PR #7105: Getting rid of some false "collision between bound variable ↵Gravatar Matthieu Sozeau2018-06-14
|\ \ \ \ | | | | | | | | | | | | | | | names" warnings
| | | | * [vernac] Add option to force building really mutual induction schemesGravatar Matthieu Sozeau2018-06-13
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Currently, if one of the inductives is non recursive, it defaults to a case analysis schems taking fewer predicates and methods just for that inductive. This irregularity prevents doing a combined scheme afterwards to gather all eliminators into one, as combined scheme expects all the eliminators to have the same predicates and methods. I have a use case in building function graphs in Equations where some of the inductives might not be recursive but I expect many other use cases could exist.
* | | | [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | | | | | | | | | | | | We move the last 3 types to more adequate places.
* | | | [api] Misctypes removal: tactic flags.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | | | | | | | | | | | | | | | | We move the "flag types" to its use place, and mark some arguments with named parameters better.
* | | | [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | | | | | | | | | | | | | | | | - move_location to proofs/logic. - intro_pattern_naming to Namegen.
* | | | [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 ↵Gravatar Maxime Dénès2018-06-05
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | vm_compute and native_compute (partial fix to #7068; also fixes #7076))
| | | * | | More straightforward native compilation of primitive projections.Gravatar Pierre-Marie Pédrot2018-06-05
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | Instead of having a constant-based compilation of projections, we generate them at the compilation time of the inductive block to which they pertain.
* | | | | 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
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | When called by auto, `simple apply` still does not respect `Opaque` because of compatibility issues.
| | * | | Preserving "canonical" form of return predicate in native_compute.Gravatar Hugo Herbelin2018-06-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note that the normalization of the context of the return predicate was not done by the native compilation but by the lazy machine. The patch also "fixes" an anomaly in the case of an arity which was not in canonical form as in: Inductive A : nat -> id (nat->Type) := . Eval native_compute in fun x => match x in A y z return y = z with end.
| | * | | Preserving "canonical" form of return predicate in vm_compute.Gravatar Hugo Herbelin2018-06-04
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note that the normalization of the context of the return predicate was not done by the vm but by the lazy machine. The patch also "fixes" an anomaly in the case of an arity which was not in canonical form as in: Inductive A : nat -> id (nat->Type) := . Eval vm_compute in fun x => match x in A y z return y = z with end.
* | | | Merge PR #7199: Fixes #7195: missing freshness condition in Ltac ↵Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ | | | | | | | | | | | | | | | pattern-matching names
* \ \ \ \ 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
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | We use an option type instead of returning a pair with a boolean. Indeed, the boolean being true was always indicating that the returned value was unchanged. The previous API was somewhat error-prone, and I don't understand why it was designed this way in the first place.
* | | | | Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ↵Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | tactic unification.
* \ \ \ \ \ 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Continuing the interface cleanup we place `Constrexpr` in the internalization module, which is the one that eliminates it. This slims down `pretyping` considerably, including removing the `Univdecls` module which existed only due to bad dependency ordering in the first place. Thanks to @ Skyskimmer we also remove a duplicate `univ_decl` definition among `Misctypes` and `UState`. This is mostly a proof of concept yet as it depends on quite a few patches of the tree. For sure some tweaks will be necessary, but it should be good for review now. IMO the tree is now in a state where we can could easy eliminate more than 10 modules without any impact, IMHO this is a net saving API-wise and would help people to understand the structure of the code better.
* | | | | | | | | Merge PR #6969: [api] Remove functions deprecated in 8.8Gravatar Maxime Dénès2018-05-31
|\ \ \ \ \ \ \ \ \
| | * | | | | | | | Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead of having the projection data in the constant data we have it independently in the environment.
* | | | | | | | | | Move interning the [hint_pattern] outside the Typeclasses hooks.Gravatar Gaëtan Gilbert2018-05-30
| |/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Close #7562. [api] move hint_info ast to tactics.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 02:18:03 +0000