| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-26 | Merge PR #8122: Fix #8119: anomalies in vm_compute with let and evars. | Maxime Dénès | |
| 2018-07-26 | Merge PR #8084: Properly disable native compilation when -native-compiler is ↵ | Maxime Dénès | |
| unset. | |||
| 2018-07-24 | Fix #8119: anomalies in vm_compute with let and evars. | Pierre-Marie Pédrot | |
| There were actually two broken things with VM + evars, the fixes are: - Do not pass let-bound arguments to evars. - Use the right order for evar arguments. Native compilation seems to be suffering from the same shortcomings, I will open a separate bug and adapt the PR. | |||
| 2018-07-24 | Add combinators to drop the bodies of local declarations. | Pierre-Marie Pédrot | |
| 2018-07-24 | Properly disable native compilation when -native-compiler is unset. | Pierre-Marie Pédrot | |
| There was a function used by the pretyper that did not check that the flag was set, leading to native compilation even when the configure flag was off. | |||
| 2018-07-24 | VM: don't duplicate projection narg information in lproj/kproj | Gaëtan Gilbert | |
| 2018-07-24 | Projections use index representation | Gaëtan Gilbert | |
| The upper layers still need a mapping constant -> projection, which is provided by Recordops. | |||
| 2018-07-24 | Merge PR #8000: Fix #7854: Native compilation + flambda trigger SEGFAULT. | Maxime Dénès | |
| 2018-07-17 | Merge PR #8055: Fast accumulator check in native compilation | Maxime Dénès | |
| 2018-07-14 | [ltac] Remove unused functions / constructors. | Emilio Jesus Gallego Arias | |
| Catched by compiling the ml files from ml4. | |||
| 2018-07-13 | Generate type-specific code for is_accu in native compilation of fixpoints. | Pierre-Marie Pédrot | |
| This is much more efficient than using Nativevalues.is_accu function which incurs a lot of irrelevant checks on its argument. | |||
| 2018-07-13 | Store the {struct} inductive type in native fixpoint AST. | Pierre-Marie Pédrot | |
| 2018-07-13 | Pass a proper environment to Nativelambda.lambda_of_constr. | Pierre-Marie Pédrot | |
| No need to roll up a new data structure when Environment has O(log n) add and lookup of rel definitions. | |||
| 2018-07-12 | Fix #7854: Native compilation + flambda trigger SEGFAULT. | Pierre-Marie Pédrot | |
| We use a more abstract representation for accumulators in the native compilation scheme, that requires less fiddling with low-level implementation details. It might be slower though. | |||
| 2018-07-03 | Term_typing: remove unused argument to internal function. | Gaëtan Gilbert | |
| The function is defined with a typo but called with the same env that is mistakenly not shadowed. An alternative to this commit would be to fix the typo. | |||
| 2018-07-03 | Cooking.cook_constant: remove unused env argument. | Gaëtan Gilbert | |
| Unused since d95306323 (remove template polymorphic definitions). | |||
| 2018-07-03 | Indtypes: remove unused is_unit. | Gaëtan Gilbert | |
| 2018-07-03 | Subtyping.check_constant: remove unused module path argument. | Gaëtan Gilbert | |
| 2018-07-03 | Inductive.extract_stack,filter_stack_domain: remove unused arguments | Gaëtan Gilbert | |
| 2018-07-03 | Nativecode compile_mind, compile_mind_field: remove unused arguments | Gaëtan Gilbert | |
| 2018-07-03 | Nativecode.pp_mllam internal pp_letrec: remove unused argument. | Gaëtan Gilbert | |
| 2018-07-03 | Modops.add_retroknowledge: remove unused argument. | Gaëtan Gilbert | |
| Unused since fe1979bf47951352ce32a6709cb5138fd26f311d. I'm not sure if it was actually used back then since I didn't look at the function it was passed to. | |||
| 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 | [env.env_rel_context.env_rel_ctx] -> [rel_context env] | Gaëtan Gilbert | |
| It's a bit shorter and more direct. | |||
| 2018-06-28 | Make Environ.globals abstract. | Gaëtan Gilbert | |
| 2018-06-27 | Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false) | Pierre-Marie Pédrot | |
| 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-27 | Merge PR #7863: Remove Sorts.contents | Pierre-Marie Pédrot | |
| 2018-06-27 | Test file for #7723 | Maxime Dénès | |
| 2018-06-27 | Fix #7723: vm_compute segfaults with universe polymorphism | Maxime Dénès | |
| Was revealing a critical bug in VM universe handling introduced in 8.5. | |||
| 2018-06-26 | Merge PR #7919: Fix equality check on global names from native compute. | Maxime Dénès | |
| 2018-06-26 | Remove Sorts.contents | Gaëtan Gilbert | |
| 2018-06-25 | Merge PR #7798: Remove hack skipping comparison of algebraic universes in ↵ | Matthieu Sozeau | |
| subtyping. | |||
| 2018-06-25 | Fix equality check on global names from native compute. | Pierre-Marie Pédrot | |
| Not sure it could have led to a soundness bug, but this is definitely serious enough to deserve a backport. Also made the code robust by listing all the constructors. | |||
| 2018-06-24 | Merge PR #7772: [native_compute] Delay computations with toplevel match | Pierre-Marie Pédrot | |
| 2018-06-23 | Merge PR #7614: Simplify the code that handles trust of side-effects in ↵ | Maxime Dénès | |
| kernel typing. | |||
| 2018-06-23 | Adapt the kernel to generate proper data for mutual records. | Pierre-Marie Pédrot | |
| Upper layers are still not able to handle mutual records though. | |||
| 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-23 | Merge PR #7715: Simplify the cooking of primitive projections. | Maxime Dénès | |
| 2018-06-22 | Merge PR #7600: Faster and cleaner fconstr-to-constr conversion function. | Maxime Dénès | |
| 2018-06-22 | Remove hack skipping comparison of algebraic universes in subtyping. | Gaëtan Gilbert | |
| When inferring [u <= v+k] I replaced the exception and instead add [u <= v]. This is trivially sound and it doesn't seem possible to have the one without the other (except specially for [Set <= v+k] which was already handled). I don't know an example where this used to fail and now succeeds (the point was to remove an anomaly, but the example ~~~ Module Type SG. Definition DG := Type. End SG. Module MG : SG. Definition DG := Type : Type. Fail End MG. ~~~ now fails with universe inconsistency. Fix #7695 (soundness bug!). | |||
| 2018-06-22 | Define and use UGraph.enforce_leq_alg for subtyping inference | Gaëtan Gilbert | |
| Not sure if worth using in other places. | |||
| 2018-06-19 | Fix Univ.enforce_leq dropped constraints when algebraic on the right | Gaëtan Gilbert | |
| There's probably a proof of false using subtyping if someone wants to look. NB: the checker doesn't handle algebraics on the right. | |||
| 2018-06-19 | Merge PR #7841: Remove Canary | Pierre-Marie Pédrot | |
| 2018-06-18 | Remove Canary. | whitequark | |
| This eliminates 3 uses of Obj from TCB. | |||
| 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 | Remove special declaration of primitive projections in the kernel. | Pierre-Marie Pédrot | |
| This reduces kernel bloat and removes code from the TCB, as compatibility projections are now retypechecked as normal definitions would have been. This should have no effect on efficiency as this only happens once at definition time. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |