| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-01-11 | COMMENTS: of "Constr.case_info" type were updated. | Matej Kosik | |
| 2016-01-11 | COMMENTS: added to the "Names.inductive" and "Names.constructor" types. | Matej Kosik | |
| 2016-01-09 | Fix bug 4479: "Error: Rewriting base foo does not exist." should be catchable. | Pierre-Marie Pédrot | |
| 2016-01-08 | Monotonizing Ftactic. | Pierre-Marie Pédrot | |
| 2016-01-08 | Be more verbose about failure to compile libraries to native code. | Guillaume Melquiond | |
| On a machine with only 1GB of memory (e.g. in a VM), the compiler might be abruptly killed by a segfault. We were not getting any feedback in that case, making it harder to debug. | |||
| 2016-01-07 | Fix a misleading comment for substn_vars | Matthieu Sozeau | |
| 2016-01-07 | Fix bug #4480: progress was not checked for setoid_rewrite. | Matthieu Sozeau | |
| Also ensure we stay compatible with 8.4: progress could now be made simply because of beta redexes in the goal. | |||
| 2016-01-06 | Fix description of command-line options in the manual. | Guillaume Melquiond | |
| 2016-01-06 | Remove deprecated command-line options such as "-as". | Guillaume Melquiond | |
| 2016-01-06 | Make code more readable by not mixing list traversal and option processing. | Guillaume Melquiond | |
| 2016-01-06 | Merge remote-tracking branch 'origin/v8.5' into trunk | Guillaume Melquiond | |
| Conflicts: lib/cSig.mli | |||
| 2016-01-06 | Prevent coq_makefile from parsing project files in the reverse order. (Fix ↵ | Guillaume Melquiond | |
| bug #4477) The bug was a bit subtle. Function process_cmd_line can be called in three different ways: 1. tail-recursively to accumulate parsed options in reverse order, 2. directly to parse a file (coqide) or a command line (coq_makefile), 3. recursively to handle a "-f" option. Once its execution finished, the function reversed its accumulator so that the parsed options are in correct order. Due to the third case, this means that the final local order of options was depending on the parity of the depth of "-f" options. This commit fixes it by changing the function so that the recursive call gets the actual accumulator rather than its reversed version. Warning: this will break all the projects that were inadvertently (or not) relying on the bug. This might also require a further commit if coq_makefile itself was relying on the bug. | |||
| 2016-01-06 | Protect code against changes in Map interface. | Maxime Dénès | |
| The Map interface of upcoming OCaml 4.03 includes a new union operator. In order to make our homemade implementation of Maps compatible with OCaml versions from 3.12 to 4.03, we define our own signatures for Maps. | |||
| 2016-01-05 | Disable warning 31 when generating coqtop from coqmktop. | Maxime Dénès | |
| In OCaml 3.x, the toploop of OCaml was accessible from toplevellib.cma. In OCaml 4.x, it was replaced by compiler-libs. However, linking with compiler-libs produces a warning (fatal with OCaml 4.03) as soon as we have a file named errors.ml or lexer.ml... The only satisfactory solution seems to be to "pack" compiler libs. But it is not done currently in the OCaml distribution, and implementing it in coqmktop at this point would be too risky. So for now, I am disabling the warning until we hear from the OCaml team. In principle, this clash of modules names can break OCaml's type safety, so we are living dangerously. | |||
| 2016-01-05 | Merge remote-tracking branch 'origin/v8.5' into trunk | Guillaume Melquiond | |
| 2016-01-05 | Avoid warning 31: test printer was linked twice with Dynlink and Str. | Maxime Dénès | |
| Linking a module twice is unsafe and warning 31 will be fatal by default in OCaml 4.03. See PR#5461. | |||
| 2016-01-05 | Fix order of files in mllib. | Maxime Dénès | |
| CString was linked after Serialize, although the later was using CString.equal. This had not been noticed so far because OCaml was ignoring functions marked as external in interfaces (which is the case of CString.equal) when considering link dependencies. This was changed on the OCaml side as part of the fix of PR#6956, so linking was now failing in several places. | |||
| 2016-01-05 | COMMENTS: Predicate | Matej Kosik | |
| In the original version, ocamldoc markup wasn't used properly thus ocamldoc output did not in all places make sense. This commit makes sure that the documentation of the Predicate module is as clear as the documentation of the Set module (in the standard library). | |||
| 2016-01-04 | fixup d2b468a, evar normalization is needed | Enrico Tassi | |
| 2016-01-04 | Extraction: msg_notice instead of msg_info. | Pierre Courtieu | |
| 2016-01-04 | Fix handling of side-effects in case of `Opaque side-effects as well. | Matthieu Sozeau | |
| 2016-01-04 | par: check if the goal is not ground and fail (fix #4465) | Enrico Tassi | |
| 2016-01-04 | workers: purge short version of -load-vernac too (fix #4458) | Enrico Tassi | |
| 2016-01-02 | Use streams rather than strings to handle bullet suggestions. | Guillaume Melquiond | |
| 2016-01-02 | Remove some unused functions. | Guillaume Melquiond | |
| Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. | |||
| 2016-01-02 | Remove keys for evar and meta, since they cannot occur. | Guillaume Melquiond | |
| 2016-01-02 | Remove some useless type declarations. | Guillaume Melquiond | |
| 2016-01-02 | Remove some useless module opening. | Guillaume Melquiond | |
| 2016-01-02 | Remove duplicate definition. | Guillaume Melquiond | |
| 2016-01-02 | Remove duplicate declarations. | Guillaume Melquiond | |
| 2016-01-02 | Reduce dependencies of interface files. | Guillaume Melquiond | |
| 2016-01-02 | Avoid warnings about loop indices. | Guillaume Melquiond | |
| 2016-01-02 | Remove useless rec flags. | Guillaume Melquiond | |
| 2016-01-02 | Simplification of grammar_prod_item type. | Pierre-Marie Pédrot | |
| Actually the identifier was never used and just carried along. | |||
| 2016-01-02 | Proper datatype for EXTEND syntax tokens. | Pierre-Marie Pédrot | |
| 2016-01-02 | Separation of concern in TacAlias API. | Pierre-Marie Pédrot | |
| The TacAlias node now only contains the arguments fed to the tactic notation. The binding variables are worn by the tactic representation in Tacenv. | |||
| 2016-01-01 | Fix typos. | Guillaume Melquiond | |
| 2016-01-01 | Remove unused hashconsing code. | Guillaume Melquiond | |
| 2016-01-01 | Do not make it harder on the compiler optimizer by packing arguments. | Guillaume Melquiond | |
| 2016-01-01 | Remove unused functions. | Guillaume Melquiond | |
| 2016-01-01 | Remove unplugged button from the interface. | Guillaume Melquiond | |
| 2016-01-01 | Remove useless recursive flags. | Guillaume Melquiond | |
| 2016-01-01 | Remove unused open. | Guillaume Melquiond | |
| 2016-01-01 | Remove duplicate declarations. | Guillaume Melquiond | |
| 2015-12-31 | Put implicits back as in 8.4. | Matthieu Sozeau | |
| 2015-12-31 | Fix bug #4456, anomaly in handle-side effects | Matthieu Sozeau | |
| The side-effects can contain universe declarations needed to typecheck later proofs, which weren't added to the env used to typecheck them. | |||
| 2015-12-31 | Remove unused function Checker.print_loc. | Guillaume Melquiond | |
| There is no location to print anyway, so it will never be useful. | |||
| 2015-12-31 | Merge branch 'v8.5' into trunk | Guillaume Melquiond | |
| 2015-12-31 | Do not compose List.length with List.filter. | Guillaume Melquiond | |
| 2015-12-31 | Remove Library.mem, which is pointless since 8.5. | Guillaume Melquiond | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |