aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
* \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-07
|\ \
| * | Remove useless debug code.Gravatar Guillaume Melquiond2016-09-02
| | |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\| |
| * | More efficient data structure to check if a native file is loaded.Gravatar Maxime Dénès2016-09-01
| | | | | | | | | | | | Spotted by PMP.
* | | CLEANUP: switching from "right-to-left" to "left-to-right" function ↵Gravatar Matej Kosik2016-08-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | composition operator. Short story: This pull-request: (1) removes the definition of the "right-to-left" function composition operator (2) adds the definition of the "left-to-right" function composition operator (3) rewrites the code relying on "right-to-left" function composition to rely on "left-to-right" function composition operator instead. Long story: In mathematics, function composition is traditionally denoted with ∘ operator. Ocaml standard library does not provide analogous operator under any name. Batteries Included provides provides two alternatives: _ % _ and _ %> _ The first operator one corresponds to the classical ∘ operator routinely used in mathematics. I.e.: (f4 % f3 % f2 % f1) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x We can call it "right-to-left" composition because: - the function we write as first (f4) will be called as last - and the function write as last (f1) will be called as first. The meaning of the second operator is this: (f1 %> f2 %> f3 %> f4) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x We can call it "left-to-right" composition because: - the function we write as first (f1) will be called first - and the function we write as last (f4) will be called last That is, the functions are written in the same order in which we write and read them. I think that it makes sense to prefer the "left-to-right" variant because it enables us to write functions in the same order in which they will be actually called and it thus better fits our culture (we read/write from left to right).
* | | CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, ↵Gravatar Matej Kosik2016-08-26
| | | | | | | | | | | | which can be useful in general, and then simplifying "Printer.pr_named_decl" function
* | | CLEANUP: rename "Context.Named.{to,of}_rel" functions to ↵Gravatar Matej Kosik2016-08-26
| | | | | | | | | | | | "Context.Named.{to,of}_rel_decl"
* | | CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"Gravatar Matej Kosik2016-08-26
| | |
* | | Merge remote-tracking branch 'v8.6' into trunkGravatar Matej Kosik2016-08-25
|\| |
* | | CLEANUP: changing the definition of the "Context.NamedList.Declaration" typeGravatar Matej Kosik2016-08-25
| | |
* | | CLEANUP: Type alias "Context.section_context" was removedGravatar Matej Kosik2016-08-25
| | |
* | | CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to ↵Gravatar Matej Kosik2016-08-25
| | | | | | | | | | | | "Context.{Rel,Named}.fold_constr"
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions. If multiple modules define a function with a same name, e.g.: Context.{Rel,Named}.get_type those calls were prefixed with a corresponding prefix to make sure that it is obvious which function is being called.
* | | Changing the definition of the "Lib.variable.info" type to enable us to do ↵Gravatar Matej Kosik2016-08-24
| | | | | | | | | | | | more cleanups
* | | Merging a branch that adds "Context.Named.Declaration.to_rel" function.Gravatar Matej Kosik2016-08-24
|\ \ \
| * | | Adding "Context.Named.Declaration.to_rel" functionGravatar Matej Kosik2016-08-24
| | | |
| | * | Use a better data structure for VM compilation of free vars.Gravatar Pierre-Marie Pédrot2016-08-22
| | | | | | | | | | | | | | | | This fixes #3450 and probably provides a huge speed-up to many instances.
| | | * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | | | | | | | | | Suggested by @ppedrot
| | | * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| |_|/ |/| | | | | | | | | | | | | | | | | As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch.
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-08-17
|\ \ \ | | |/ | |/|
* | | Revert "CLEANUP: removing the definition of the ↵Gravatar Pierre-Marie Pédrot2016-08-17
| |/ |/| | | | | | | | | | | | | | | | | | | "Context.Rel.Declaration.to_tuple" function" This reverts commit 4b24bb7d3b770592015c264001b9aed9fe95c200. While the of_tuple function is clearly dubious and mostly used for compatiblity reasons, and thus had to be removed, I think that the to_tuple function is still useful as it allows to access each component of the declaration piecewise. Without it, some codes tend to get cluttered with useless projections here and there.
* | Adding "Context.Named.Declaraton.of_rel" functionGravatar Matej Kosik2016-08-11
| |
* | CLEANUP: removing the definition of the "Context.Rel.Declaration.of_tuple" ↵Gravatar Matej Kosik2016-08-11
| | | | | | | | function
* | CLEANUP: removing the definition of the "Context.Rel.Declaration.to_tuple" ↵Gravatar Matej Kosik2016-08-11
| | | | | | | | function
| * Make code a bit clearer by removing optional argument.Gravatar Guillaume Melquiond2016-08-10
|/
* Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-26
|\
| * Fix bug #4876: critical bug in guard condition checker.Gravatar Matthieu Sozeau2016-07-25
| |
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\|
| * Prevent unsafe overwriting of Required modules by toplevel library.Gravatar Maxime Dénès2016-07-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In coqtop, one could do for instance: Require Import Top. (* Where Top contains a Definition b := true *) Lemma bE : b = true. Proof. reflexivity. Qed. Definition b := false. Lemma bad : False. Proof. generalize bE; compute; discriminate. Qed. That proof could however not be saved because of the circular dependency check. Safe_typing now checks that we are not requiring (Safe_typing.import) a library with the same logical name as the current one.
| * congruence: Restrict refreshing to SetGravatar Matthieu Sozeau2016-07-04
| | | | | | | | | | | | Because refreshing Prop is not semantics-preserving, the new universe is >= Set, so cannot be minimized to Prop afterwards.
* | closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
| | | | | | | | For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | | | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a reimplementation of Hugo's PR#117. We are trying to address the problem that the name of some reduction functions was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in reduction). Like PR#117, we are careful that no function changed semantics without changing the names. Porting existing ML code should be a matter of renamings a few function calls. Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX collectively denominated iota. We renamed the following functions: Closure.betadeltaiota -> Closure.all Closure.betadeltaiotanolet -> Closure.allnolet Reductionops.beta -> Closure.beta Reductionops.zeta -> Closure.zeta Reductionops.betaiota -> Closure.betaiota Reductionops.betaiotazeta -> Closure.betaiotazeta Reductionops.delta -> Closure.delta Reductionops.betalet -> Closure.betazeta Reductionops.betadelta -> Closure.betadeltazeta Reductionops.betadeltaiota -> Closure.all Reductionops.betadeltaiotanolet -> Closure.allnolet Closure.no_red -> Closure.nored Reductionops.nored -> Closure.nored Reductionops.nf_betadeltaiota -> Reductionops.nf_all Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta Reductionops.whd_betadeltaiota -> Reductionops.whd_all Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state Reductionops.whd_eta -> Reductionops.shrink_eta Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all And removed the following ones: Reductionops.whd_betaetalet Reductionops.whd_betaetalet_stack Reductionops.whd_betaetalet_state Reductionops.whd_betadeltaeta_stack Reductionops.whd_betadeltaeta_state Reductionops.whd_betadeltaeta Reductionops.whd_betadeltaiotaeta_stack Reductionops.whd_betadeltaiotaeta_state Reductionops.whd_betadeltaiotaeta They were unused and having some reduction functions perform eta is confusing as whd_all and nf_all don't do it.
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* | Shrink Proofs/Obligations by default and deprecateGravatar Matthieu Sozeau2016-06-27
| | | | | | | | | | | | | | | | | | Fix bug in Shrink obligations with Program in the process. Fix implementation of shrink for abstract proofs - Update doc in term.mli to reflect the fact that let-in's are part of what is returned by [decompose_lam_assum].
* | [feedback] Add optional ?loc parameter to loggers.Gravatar Emilio Jesus Gallego Arias2016-06-25
| | | | | | | | | | | | | | | | This is a first step to relay location info in an uniform way, as needed by warnings and other mechanisms. The location info remains unused for now, but coqtop printing could take advantage of it if so wished.
* | Fix bug #4825: [clear] should not dependency-check hypotheses that come ↵Gravatar Pierre-Marie Pédrot2016-06-20
| | | | | | | | above it.
* | Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
| |
* | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
| |
* | Adding a local type-in-type flag in kernel declarations.Gravatar Pierre-Marie Pédrot2016-06-18
| |
* | Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
| | | | | | | | | | This allows a smooth addition of various unsafe flags without wreaking havoc in the ML codebase.
* | Adding a default safe set of kernel typing flags to Declareops.Gravatar Pierre-Marie Pédrot2016-06-16
| |
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
| * | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
| | | | | | | | | | | | | | | | | | | | | The rational is that 1. further typing flags may be available in the future 2. it makes it easier to trace and document the argument
* | | newring: fix for hack using evars as integers.Gravatar Matthieu Sozeau2016-06-09
| | |
* | | Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
| | |
* | | Please never mention .mli-only file in *.mllib (or future *.mlpack)Gravatar Pierre Letouzey2016-06-02
| | | | | | | | | | | | | | | This breaks compilation via ocamlbuild, and also leads to awkward commands via make
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\ \ \ | | |/ | |/|
| * | Fix potential race condition in vm_compute.Gravatar Guillaume Melquiond2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | If the second allocation causes a collection of the minor heap, the first allocation will be freed, thus causing a memory corruption. Note: it only happens when computing the native projection of an opaque value while the minor heap is almost full.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 19:45:34 +0000