| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-15 | Merge PR #1037: Parse directly to Sorts.family when appropriate. | Maxime Dénès | |
| 2017-09-15 | Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match ↵ | Maxime Dénès | |
| anonymous variables) | |||
| 2017-09-08 | Parse directly to Sorts.family when appropriate. | Gaëtan Gilbert | |
| When we used to parse to a glob_sort but always give an empty list in the GType case we can now parse directly to Sorts.family. | |||
| 2017-09-04 | Making detyping potentially lazy. | Pierre-Marie Pédrot | |
| The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager. | |||
| 2017-08-31 | Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name | Maxime Dénès | |
| 2017-08-31 | Merge PR #995: Program: fix BZ#5683, missing lift when building case predicate | Maxime Dénès | |
| 2017-08-31 | Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flag | Maxime Dénès | |
| 2017-08-31 | Merge PR #989: Prevent overallocation in Array.map_to_list and remove custom ↵ | Maxime Dénès | |
| implementation from Detyping. | |||
| 2017-08-29 | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170 | Maxime Dénès | |
| 2017-08-29 | Merge PR #946: Functional pretyping interface | Maxime Dénès | |
| 2017-08-29 | Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map | Hugo Herbelin | |
| (from module List). | |||
| 2017-08-25 | primproj: fix bug 5245, hnf on proj with simpl never flag. | Matthieu Sozeau | |
| 2017-08-24 | Program: fix BZ#5683, missing lift when building case predicate | Matthieu Sozeau | |
| 2017-08-22 | use OCaml 4.03-compatible Filename functions | Paul Steckler | |
| 2017-08-22 | Prevent overallocation in Array.map_to_list and remove custom implementation ↵ | Guillaume Melquiond | |
| from Detyping. | |||
| 2017-08-18 | use OCaml temp_file, instead of our own version | Paul Steckler | |
| 2017-08-18 | move filename search to start_profiler | Paul Steckler | |
| 2017-08-17 | Add native compute profiling, BZ#5170 | Paul Steckler | |
| 2017-08-16 | Merge PR #841: Timorous fix of bug #5598 on global existing class in sections | Maxime Dénès | |
| 2017-08-01 | Remove understand_tcc_evars. | Maxime Dénès | |
| Use the functional interface understand_tcc instead. | |||
| 2017-08-01 | Move type_uconstr to Tacinterp. | Maxime Dénès | |
| 2017-08-01 | Remove understand_judgment and understand_judgment_tcc. | Maxime Dénès | |
| 2017-08-01 | Remove allow_anonymous_refs. | Maxime Dénès | |
| 2017-08-01 | Remove pure_open_constr (now open_constr) | Maxime Dénès | |
| 2017-08-01 | Move glob_constr_ltac_closure to evar_refiner. | Maxime Dénès | |
| 2017-08-01 | Merge PR #913: Less allocations in Detyping | Maxime Dénès | |
| 2017-08-01 | Merge PR #806: closing bug 5315 | Maxime Dénès | |
| 2017-07-31 | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | Maxime Dénès | |
| 2017-07-29 | closing bug 5315 | Julien Forest | |
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík | |
| 2017-07-26 | Add a comment regarding the specialization of the combinator in Detyping. | Pierre-Marie Pédrot | |
| 2017-07-26 | Removing template polymorphism for definitions. | Pierre-Marie Pédrot | |
| The use of template polymorphism in constants was quite limited, as it only applied to definitions that were exactly inductive types without any parameter whatsoever. Furthermore, it seems that following the introduction of polymorphic definitions, the code path enforced regular polymorphism as soon as the type of a definition was given, which was in practice almost always. Removing this feature had no observable effect neither on the test-suite, nor on any development that we monitor on Travis. I believe it is safe to assume it was nowadays useless. | |||
| 2017-07-21 | Allocation-friendly detyping of term arrays. | Pierre-Marie Pédrot | |
| This is important for externalization big terms. We were indeed allocating twice as much as needed lists for the application node case, as the Array.map_to_list function is exactly List.map o Array.to_list. We could probably tweak this function instead, at the expense that order of evaluation is not guaranteed. I'm not willing to do that though. | |||
| 2017-07-20 | Merge branch 'v8.7' | Maxime Dénès | |
| 2017-07-13 | Remove the function Global.type_of_global_unsafe. | Pierre-Marie Pédrot | |
| 2017-07-13 | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global. | Pierre-Marie Pédrot | |
| 2017-07-13 | Getting rid of AUContext abstraction breakers in Discharge. | Pierre-Marie Pédrot | |
| 2017-07-13 | Make the typeclass implementation fully compatible with universe polymorphism. | Pierre-Marie Pédrot | |
| This essentially means storing the abstract universe context in the typeclass data, and abstracting it when necessary. | |||
| 2017-07-13 | Safer API for Global.type_of_global_in_context. | Pierre-Marie Pédrot | |
| We return the abstract context instead of an arbitrary instantiation. | |||
| 2017-07-13 | Getting rid of AUContext abstraction breakers in Recordops. | Pierre-Marie Pédrot | |
| 2017-07-13 | Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel | Maxime Dénès | |
| 2017-07-11 | Deprecate options that were introduced for compatibility with 8.5. | Théo Zimmermann | |
| 2017-07-11 | Safe API for accessing universe constraints of global references. | Pierre-Marie Pédrot | |
| Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel. | |||
| 2017-07-11 | Less footguns in universe handling: remove subst_instance_context. | Pierre-Marie Pédrot | |
| This function was lurking around, waiting to bite anybody willing to use it. We use instead a better API, correct and much less error-prone. | |||
| 2017-07-11 | Getting rid of simple calls to AUContext.instance. | Pierre-Marie Pédrot | |
| This function breaks the abstraction barrier of abstract universe contexts, as it provides a way to observe the bound names of such a context. We remove all the uses that can be easily get rid of with the current API. | |||
| 2017-07-07 | Merge PR #863: Fixing environment in warning "Projection value has no head ↵ | Maxime Dénès | |
| constant". | |||
| 2017-07-07 | Fixing environment in warning "Projection value has no head constant". | Hugo Herbelin | |
| Delaying also some computation needed for printing to the time of really printing it. | |||
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2017-06-28 | A fix for #5598 (no discharge of Existing Classes referring to local variables). | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |