aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-08-30CLEANUP: switching from "right-to-left" to "left-to-right" function ↵Matej Kosik
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).
2016-08-30CLEANUP: using |> operator more consistentlyMatej Kosik
2016-08-30CLEANUP: removing a function that duplicates its counterpart already present ↵Matej Kosik
in the Ocaml standard library
2016-08-30Setting an unknown option now always a warning. Fixes #4947.Maxime Dénès
Previously, setting an unknown option was an error or a warning, depending on the type of the option. We make it always a warning, for forward compatibility. This was already fixed in 8.6.
2016-08-29CLEANUP: taking advantage of "_ % _" operator to express function ↵Matej Kosik
composition in a more obvious way This commit rewrites terms (fun x -> f1 (f2 ... (fN x)...)) to f1 % f2 % ... % fN
2016-08-29Fix bug #4421: Messages dialog in Coqide resets.Pierre-Marie Pédrot
2016-08-29CoqIDE preserves unknown preferences.Pierre-Marie Pédrot
This allows a smoother transition between various versions of CoqIDE, by not erasing options which are unknown at the present time.
2016-08-29Fix tagging of notations.Pierre-Marie Pédrot
We only tag the non-whitespace substrings, rather than the whole terminal token.
2016-08-29Fix inefficiency in CoqIDE display of tagged text.Pierre-Marie Pédrot
The helper code in LablGTK is algorithmically slow, so that we rather reimplement it as a small helper function.
2016-08-29Send Dependency feedback only if file not already loaded.Maxime Dénès
2016-08-28Fix bug #4750: Change format of inconsistent assumptions message.Pierre-Marie Pédrot
We now print the file responsible for the incompatibility in require error messages.
2016-08-28Fix bug #4764: Syntactic notation externalization breaks.Pierre-Marie Pédrot
2016-08-27Support qualified identifiers in Show Match (bug #5050).Guillaume Melquiond
2016-08-26Removing calls of "Context.Rel.Declaration.to_tuple" functionMatej Kosik
2016-08-26CLEANUP: minor readability improvementsMatej Kosik
2016-08-26CLEANUP: removing "Termops.compact_named_context_reverse" functionMatej Kosik
2016-08-26CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, ↵Matej Kosik
which can be useful in general, and then simplifying "Printer.pr_named_decl" function
2016-08-26CLEANUP: rename "Context.Named.{to,of}_rel" functions to ↵Matej Kosik
"Context.Named.{to,of}_rel_decl"
2016-08-26CLEANUP: renaming "Printer.pr_var_decl" function to "Printer.pr_named_decl"Matej Kosik
2016-08-26CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"Matej Kosik
2016-08-25FIX: Coq versionMatej Kosik
2016-08-25Merge remote-tracking branch 'v8.6' into trunkMatej Kosik
2016-08-25FIX: Coq versionMatej Kosik
2016-08-25CLEANUP: changing the definition of the "Context.NamedList.Declaration" typeMatej Kosik
2016-08-25CLEANUP: Type alias "Context.section_context" was removedMatej Kosik
2016-08-25CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to ↵Matej Kosik
"Context.{Rel,Named}.fold_constr"
2016-08-25Do not export an internal function in Namegen.Pierre-Marie Pédrot
2016-08-25CLEANUP: removing calls of the "Context.Named.Declaration.get_value" functionMatej Kosik
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
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.
2016-08-24CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionMatej Kosik
2016-08-24CLEANUP: removing superfluous (module) qualifiersMatej Kosik
2016-08-24CLEANUP: removing unnecessary variable bindingMatej Kosik
2016-08-24Changing the definition of the "Lib.variable.info" type to enable us to do ↵Matej Kosik
more cleanups
2016-08-24Merging a branch that adds "Context.Named.Declaration.to_rel" function.Matej Kosik
2016-08-24Adding "Context.Named.Declaration.to_rel" functionMatej Kosik
2016-08-24Properly compute types for assumed section variables (bug #5035).Guillaume Melquiond
This bug was introduced by commit 34ef02fac1110673ae74c41c185c228ff7876de2 Author: Matej Kosik <m4tej.kosik@gmail.com> Date: Fri Jan 29 10:13:12 2016 +0100 CLEANUP: Context.{Rel,Named}.Declaration.t
2016-08-24Merge PR #260: "Fix bug 4842 (Time prints in multiple lines)" into v8.6Pierre-Marie Pédrot
2016-08-24Merge PR #258: "Fix newline issues" into v8.6Pierre-Marie Pédrot
2016-08-23Fix bug #4914: LtacProf printout has too many newlines.Pierre-Marie Pédrot
2016-08-23Arguments: give / after last ! error detection fixedEnrico Tassi
2016-08-23fix get_host_port error message (#4724)Enrico Tassi
2016-08-23update Proof General URLPaul Steckler
2016-08-23Fix bug #4904: [Import] does not load intermediately unqualified names of ↵Pierre-Marie Pédrot
aliases.
2016-08-22Fast path for set operations.Pierre-Marie Pédrot
We consider an approximation of the size of sets before choosing the most appropriate algorithm. This drastically affects some universe-polymorphic code which was doing a lot of set operations on disimilar sizes.
2016-08-22Merge remote-tracking branch 'github/pr/261' into v8.6Maxime Dénès
Was PR#261: Use a better data structure for VM compilation of free vars.
2016-08-22Use a better data structure for VM compilation of free vars.Pierre-Marie Pédrot
This fixes #3450 and probably provides a huge speed-up to many instances.
2016-08-22Pushing error backtrace in unification reraise.Pierre-Marie Pédrot
2016-08-21Documenting "Set Structural Injection".Hugo Herbelin
2016-08-21Do not recompute the whole evar naming environment in GProd intepretation.Pierre-Marie Pédrot
2016-08-21Short path for Pretyping.ltac_interp_name_env.Pierre-Marie Pédrot
Instead of recomputing the evar name environment from scratch when it is unchanged, we simply return the original one. This should fix #4964 for good, although I still find the global evar naming mechanism from Pretyping more than messy. Introducing the heuristic allowing to capture variables from Ltac in constr binders is indeed the root of many evils... That is far from being a zero-cost abstraction!
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 11:24:46 +0000