| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-09-01 | Notation_ops.subst_glob_vars: substituting also in evar kind for | Hugo Herbelin | |
| consistency of the use of names. | |||
| 2016-09-01 | Short documentation, filling TODO's in evd.mli. | Hugo Herbelin | |
| 2016-09-01 | Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior). | Hugo Herbelin | |
| (It was reducing also in hypotheses.) | |||
| 2016-09-01 | Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internal | Hugo Herbelin | |
| calls are logged too. Using appropriate printer for reparsability of the output. | |||
| 2016-09-01 | Fixing name of internal refine ("simple refine"). | Hugo Herbelin | |
| 2016-08-31 | Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'. | Frédéric Besson | |
| If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative. | |||
| 2016-08-31 | Fix bug #5043: [Admitted] lemmas pick up section variables. | Pierre-Marie Pédrot | |
| We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables. | |||
| 2016-08-30 | Fix bug #5051: Large outputs are garbled. | Pierre-Marie Pédrot | |
| Instead of relying on the current position of the cursor, we rather use a dedicated mark in the message view. | |||
| 2016-08-30 | Fixing output test-suite after warning for inner Requires. | Pierre-Marie Pédrot | |
| 2016-08-30 | Fix bug #4893: not_evar: unexpected failure in 8.5pl1. | Pierre-Marie Pédrot | |
| 2016-08-30 | plugin micromega : nra also handles non-linear rational arithmetic over Q ↵ | Frédéric Besson | |
| (Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R. | |||
| 2016-08-30 | Fix bug #3920: eapply masks an hypothesis name. | Pierre-Marie Pédrot | |
| The problem came from the fact that the legacy beta-reduction occurring after a rewrite was wrongly applied to the side-conditions of the rewriting step. We restrict it to the correct goal in this patch. | |||
| 2016-08-30 | Emit a warning on Require inside a module. | Maxime Dénès | |
| 2016-08-30 | Fix #4941 - ~/.coqrc file confusing locations | Maxime Dénès | |
| 2016-08-30 | Fix #4871 - interrupting par:abstract kills coqtop | Maxime Dénès | |
| Fix done with Enrico. | |||
| 2016-08-30 | Missing .PHONY targets. | Pierre-Marie Pédrot | |
| 2016-08-30 | micromega cache files are now hidden files (cf #4156) | Frédéric Besson | |
| csdp.cache -> .csdp.cache lia.cache -> .lia.cache nlia.cache -> .nia.cache | |||
| 2016-08-30 | CLEANUP: 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-30 | CLEANUP: using |> operator more consistently | Matej Kosik | |
| 2016-08-30 | CLEANUP: removing a function that duplicates its counterpart already present ↵ | Matej Kosik | |
| in the Ocaml standard library | |||
| 2016-08-30 | Setting 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-29 | CLEANUP: 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-29 | Fix bug #4421: Messages dialog in Coqide resets. | Pierre-Marie Pédrot | |
| 2016-08-29 | CoqIDE 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-29 | Fix tagging of notations. | Pierre-Marie Pédrot | |
| We only tag the non-whitespace substrings, rather than the whole terminal token. | |||
| 2016-08-29 | Fix 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-29 | Send Dependency feedback only if file not already loaded. | Maxime Dénès | |
| 2016-08-28 | Fix 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-28 | Fix bug #4764: Syntactic notation externalization breaks. | Pierre-Marie Pédrot | |
| 2016-08-27 | Support qualified identifiers in Show Match (bug #5050). | Guillaume Melquiond | |
| 2016-08-26 | Removing calls of "Context.Rel.Declaration.to_tuple" function | Matej Kosik | |
| 2016-08-26 | CLEANUP: minor readability improvements | Matej Kosik | |
| 2016-08-26 | CLEANUP: removing "Termops.compact_named_context_reverse" function | Matej Kosik | |
| 2016-08-26 | CLEANUP: 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-26 | CLEANUP: rename "Context.Named.{to,of}_rel" functions to ↵ | Matej Kosik | |
| "Context.Named.{to,of}_rel_decl" | |||
| 2016-08-26 | CLEANUP: renaming "Printer.pr_var_decl" function to "Printer.pr_named_decl" | Matej Kosik | |
| 2016-08-26 | CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted" | Matej Kosik | |
| 2016-08-25 | FIX: Coq version | Matej Kosik | |
| 2016-08-25 | Merge remote-tracking branch 'v8.6' into trunk | Matej Kosik | |
| 2016-08-25 | FIX: Coq version | Matej Kosik | |
| 2016-08-25 | CLEANUP: changing the definition of the "Context.NamedList.Declaration" type | Matej Kosik | |
| 2016-08-25 | CLEANUP: Type alias "Context.section_context" was removed | Matej Kosik | |
| 2016-08-25 | CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to ↵ | Matej Kosik | |
| "Context.{Rel,Named}.fold_constr" | |||
| 2016-08-25 | Do not export an internal function in Namegen. | Pierre-Marie Pédrot | |
| 2016-08-25 | CLEANUP: removing calls of the "Context.Named.Declaration.get_value" function | Matej Kosik | |
| 2016-08-24 | CLEANUP: minor readability improvements | Matej 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-24 | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function | Matej Kosik | |
| 2016-08-24 | CLEANUP: removing superfluous (module) qualifiers | Matej Kosik | |
| 2016-08-24 | CLEANUP: removing unnecessary variable binding | Matej Kosik | |
| 2016-08-24 | Changing the definition of the "Lib.variable.info" type to enable us to do ↵ | Matej Kosik | |
| more cleanups | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |