aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* change into QuestionMark defaultGravatar Siddharth Bhat2018-07-17
|
* Change QuestionMark for better record field missing error message.Gravatar Siddharth Bhat2018-07-17
| | | | | | | | | | While we were adding a new field into `QuestionMark`, we decided to go ahead and refactor the constructor to hold an actual record. This record now holds the name, obligations, and whether the evar represents a missing record field. This is used to provide better error messages on missing record fields.
* 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
| |/ |/| | | | | | | | | In #7607, dead code that used to handle non-dependent return predicates was removed. This made the reification branch expecting non-functions in predicates dead code. We fix this by using an assert instead.
* | 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
| | | | | | | | | | | | (Universes and Evd)
* | | Merge PR #7607: Simplify reification of predicate in bytecode and native ↵Gravatar Pierre-Marie Pédrot2018-07-03
|\ \ \ | |/ / |/| | | | | compilers
* | | 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
| | | |
| | * | Simplify reification of predicate in bytecode and native compilersGravatar Maxime Dénès2018-06-28
| |/ / |/| | | | | | | | | | | I believe this is legacy code due to a previous, more complex representation of return predicates in the kernel.
* | | 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.
| | * Fix #5719: Uncaught exception Invalid_argument.Gravatar Pierre-Marie Pédrot2018-06-21
| | | | | | | | | | | | | | | | | | It seems that lifting a term with a negative index is not equivalent to strengthening it by applying to a dummy substitution. This looks suspicious at best.
* | | 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 16:14:55 +0000