| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-17 | change into QuestionMark default | Siddharth Bhat | |
| 2018-07-17 | Change QuestionMark for better record field missing error message. | Siddharth Bhat | |
| 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. | |||
| 2018-07-10 | Merge PR #7983: Turn a dead branch into an assertion failure in VM reification. | Maxime Dénès | |
| 2018-07-09 | Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument. | Matthieu Sozeau | |
| 2018-07-05 | Turn a dead branch into an assertion failure in VM reification. | Pierre-Marie Pédrot | |
| 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. | |||
| 2018-07-05 | Merge PR #7746: Many small cleanups removing unused arguments and functions | Pierre-Marie Pédrot | |
| 2018-07-03 | Glob_ops.rename_glob_vars: fix typo | Gaëtan Gilbert | |
| 2018-07-03 | Glob_ops.fix_kind_eq: fix typo | Gaëtan Gilbert | |
| 2018-07-03 | Remove unused env argument to fresh_sort_in_family | Gaëtan Gilbert | |
| (Universes and Evd) | |||
| 2018-07-03 | Merge PR #7607: Simplify reification of predicate in bytecode and native ↵ | Pierre-Marie Pédrot | |
| compilers | |||
| 2018-06-29 | Merge PR #7080: Swapping Context and Constr and defining declarations on ↵ | Maxime Dénès | |
| constr in Constr | |||
| 2018-06-28 | Deprecate Environ.retroknowledge function in favor of the projection | Gaëtan Gilbert | |
| 2018-06-28 | Simplify reification of predicate in bytecode and native compilers | Maxime Dénès | |
| I believe this is legacy code due to a previous, more complex representation of return predicates in the kernel. | |||
| 2018-06-28 | Merge PR #7866: Implementation of mutual records in the higher strata | Maxime Dénès | |
| 2018-06-27 | Swapping Context and Constr: defining declarations on constr in Constr. | Hugo Herbelin | |
| 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). | |||
| 2018-06-26 | Remove Sorts.contents | Gaëtan Gilbert | |
| 2018-06-24 | Handle mutual records in upper layers. | Pierre-Marie Pédrot | |
| 2018-06-23 | Merge PR #7827: [engine] safe [add_unification_pb] interface | Pierre-Marie Pédrot | |
| 2018-06-23 | Using more general information for primitive records. | Pierre-Marie Pédrot | |
| This brings more compatibility with handling of mutual primitive records in the kernel. | |||
| 2018-06-23 | Change the proj_ind field from MutInd.t to inductive. | Pierre-Marie Pédrot | |
| This is a first step towards the acceptance of mutual record types in the kernel. | |||
| 2018-06-21 | Fix #5719: Uncaught exception Invalid_argument. | Pierre-Marie Pédrot | |
| 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. | |||
| 2018-06-21 | Rename Dyn.TParam→ValueS, Dyn.MapS.obj→value to clarify their purpose. | whitequark | |
| 2018-06-19 | Merge PR #7797: Remove reference name type. | Enrico Tassi | |
| 2018-06-19 | Merge PR #6754: Better elaboration of pattern-matchings on primitive projections | Pierre-Marie Pédrot | |
| 2018-06-19 | Merge PR #7801: [vernac] Add option to force building really mutual ↵ | Enrico Tassi | |
| induction schemes | |||
| 2018-06-19 | Merge PR #7714: Remove primitive-projection related data from the kernel | Maxime Dénès | |
| 2018-06-18 | Remove reference name type. | Maxime Dénès | |
| 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. | |||
| 2018-06-17 | Remove the proj_body field from the kernel. | Pierre-Marie Pédrot | |
| 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. | |||
| 2018-06-17 | Remove the proj_eta field of the kernel. | Pierre-Marie Pédrot | |
| 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. | |||
| 2018-06-17 | Fixes #7811 (uncaught Not_found in notation printer related to "match"). | Hugo Herbelin | |
| 2018-06-15 | Better elaboration of pattern-matchings on primitive projections | Matthieu Sozeau | |
| This ensures that computations are shared as much as possible, mimicking the "positive" records computational behavior if possible. | |||
| 2018-06-15 | evd/evarutil: safe [add_unification_pb] interface, taking EConstr's | Matthieu Sozeau | |
| Avoid adding the same unification problem twice, module evar instantiation. | |||
| 2018-06-14 | Fix deprecation warning introduced by PR 664 merge | Matthieu Sozeau | |
| 2018-06-14 | Merge PR #664: Fixing #5500 (missing test in return clause of match leading ↵ | Matthieu Sozeau | |
| to anomaly) | |||
| 2018-06-14 | Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder ↵ | Matthieu Sozeau | |
| in unification | |||
| 2018-06-14 | Merge PR #7105: Getting rid of some false "collision between bound variable ↵ | Matthieu Sozeau | |
| names" warnings | |||
| 2018-06-13 | [vernac] Add option to force building really mutual induction schemes | Matthieu Sozeau | |
| 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. | |||
| 2018-06-12 | [api] Remove Misctypes. | Emilio Jesus Gallego Arias | |
| We move the last 3 types to more adequate places. | |||
| 2018-06-12 | [api] Misctypes removal: tactic flags. | Emilio Jesus Gallego Arias | |
| We move the "flag types" to its use place, and mark some arguments with named parameters better. | |||
| 2018-06-12 | [api] Misctypes removal: several moves: | Emilio Jesus Gallego Arias | |
| - move_location to proofs/logic. - intro_pattern_naming to Namegen. | |||
| 2018-06-12 | [api] Misctypes removal: remove dummy alias. | Emilio Jesus Gallego Arias | |
| 2018-06-12 | [api] Misctypes removal: miscellaneous aliases. | Emilio Jesus Gallego Arias | |
| 2018-06-12 | Fixes #7780 (missing lift in expanding alias under a binder in unification). | Hugo Herbelin | |
| 2018-06-05 | Merge PR #7679: Clean native compilation of primitive projections | Maxime Dénès | |
| 2018-06-05 | Merge PR #7004: Make `simple apply` obey `Opaque` directive. | Pierre-Marie Pédrot | |
| 2018-06-05 | Merge PR #7077: Preserving canonical structure of return predicate in ↵ | Maxime Dénès | |
| vm_compute and native_compute (partial fix to #7068; also fixes #7076)) | |||
| 2018-06-05 | More straightforward native compilation of primitive projections. | Pierre-Marie Pédrot | |
| Instead of having a constant-based compilation of projections, we generate them at the compilation time of the inductive block to which they pertain. | |||
| 2018-06-05 | Merge PR #7099: Stronger invariants in unification signature. | Matthieu Sozeau | |
| 2018-06-05 | Make direct invocations of `simple apply` obey `Opaque` directive. | Maxime Dénès | |
| When called by auto, `simple apply` still does not respect `Opaque` because of compatibility issues. | |||
| 2018-06-04 | Preserving "canonical" form of return predicate in native_compute. | Hugo Herbelin | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |