aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Temporary commit getting rid of Obj.magic unsafety for Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
| | | | This will allow an easier landing of the rewriting of Genarg.
* Removing dynamic entries from Pcoq.Gravatar Pierre-Marie Pédrot2016-01-17
|
* ML extensions use untyped representation of user entries.Gravatar Pierre-Marie Pédrot2016-01-17
|
* Separating the parsing of user-defined entries from their intepretation.Gravatar Pierre-Marie Pédrot2016-01-16
|
* Less type-unsafety in Pcoq.Gravatar Pierre-Marie Pédrot2016-01-16
|
* Tactic notation printing accesses all the token data.Gravatar Pierre-Marie Pédrot2016-01-16
|
* Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
|
* Removing ident and var generic arguments.Gravatar Pierre-Marie Pédrot2016-01-14
|
* Moving is_quantified_hypothesis to new proof engine.Gravatar Hugo Herbelin2016-01-14
|
* Updating and improving the documentation of intros patterns.Gravatar Hugo Herbelin2016-01-14
| | | | In particular, documenting bracketing of last pattern on by default.
* Continuing 003fe3d5e on parsing positions.Gravatar Hugo Herbelin2016-01-14
| | | | | | | - Being stricter on the ordinal suffix accepted (only st for 1, 21, etc, nd for 2, 22, etc., etc.) - Reporting when the suffix is not the expected one (rather than considering that, e.g. 2st, is two tokens, a number then an identifier).
* Changing "P is assumed" to "P is declared".Gravatar Hugo Herbelin2016-01-14
| | | | | | | | The term "assumed" refers more to the type of the object than to the name of the object. It is particularly misguiding when P:Prop since P is assumed would suggest that a proof of P is assumed, and not that the variable P itself is declared (see discussion with P. Castéran on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015).
* Update in the documentation of parts of the code of destruct/induction.Gravatar Hugo Herbelin2016-01-14
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\
| * Fixing success of test for #3848 after move to directory "closed".Gravatar Hugo Herbelin2016-01-13
| |
| * Fixing #4467 (continued).Gravatar Hugo Herbelin2016-01-13
| | | | | | | | | | Function is_constructor was not properly fixed. Additionally, this fixes a problem with the 8.5 interpretation of in-pattern (see Cases.v).
| * Fixing #4467 (missing shadowing of variables in cases pattern).Gravatar Hugo Herbelin2016-01-12
| | | | | | | | | | This fixes a TODO in map_constr_expr_with_binders, a bug in is_constructor, as well as a bug and TODOS in ids_of_cases_indtype.
| * Fixing #4256 and #4484 (changes in evar-evar resolution made that newGravatar Hugo Herbelin2016-01-12
| | | | | | | | | | | | | | | | evars were created making in turn that evars formerly recognized as pending were not anymore in the list of pending evars). This also fixes the reopening of #3848. See comments on #4484 for details.
| * Reporting about the new tactical unshelve.Gravatar Hugo Herbelin2016-01-12
| |
| * Extend last commit: keyed unification uses full conversions on the applied ↵Gravatar Matthieu Sozeau2016-01-12
| | | | | | | | constant and arguments _separately_.
| * Extend Keyed Unification tests with the one from R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
| |
| * Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
| | | | | | | | | | [rewrite] was calling find_suterm using the wrong unification flags, not allowing full delta in unification of terms with the right keys as desired.
| * Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.Gravatar Hugo Herbelin2016-01-12
| |
| * Documenting dtauto and dintuition.Gravatar Hugo Herbelin2016-01-12
| |
| * Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".Gravatar Hugo Herbelin2016-01-12
| |
| * Documenting option 'Set Bracketing Last Introduction Pattern'.Gravatar Hugo Herbelin2016-01-12
| |
| * restore documentation of admitGravatar Enrico Tassi2016-01-12
| |
* | CLEANUP: removing unnecessary wrapperGravatar Matej Kosik2016-01-11
| |
* | COMMENTS: added to the "Constrexpr.CCases" variant.Gravatar Matej Kosik2016-01-11
| |
* | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
| | | | | | | | | | | | | | I have removed the second field of the "Constrexpr.CRecord" variant because once it was set to "None" it never changed to anything else. It was just carried and copied around.
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
| | * Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.Gravatar Matthieu Sozeau2016-01-11
| | |
* | | COMMENTS: of "Constr.case_info" type were updated.Gravatar Matej Kosik2016-01-11
| | |
* | | COMMENTS: added to the "Names.inductive" and "Names.constructor" types.Gravatar Matej Kosik2016-01-11
| | |
* | | Fix bug 4479: "Error: Rewriting base foo does not exist." should be catchable.Gravatar Pierre-Marie Pédrot2016-01-09
| | |
* | | Monotonizing Ftactic.Gravatar Pierre-Marie Pédrot2016-01-08
| | |
| | * Be more verbose about failure to compile libraries to native code.Gravatar Guillaume Melquiond2016-01-08
| | | | | | | | | | | | | | | | | | 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.
| | * Fix a misleading comment for substn_varsGravatar Matthieu Sozeau2016-01-07
| | |
| | * Fix bug #4480: progress was not checked for setoid_rewrite.Gravatar Matthieu Sozeau2016-01-07
| | | | | | | | | | | | | | | Also ensure we stay compatible with 8.4: progress could now be made simply because of beta redexes in the goal.
| | * Fix description of command-line options in the manual.Gravatar Guillaume Melquiond2016-01-06
| | |
* | | Remove deprecated command-line options such as "-as".Gravatar Guillaume Melquiond2016-01-06
| | |
* | | Make code more readable by not mixing list traversal and option processing.Gravatar Guillaume Melquiond2016-01-06
| | |
* | | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-06
|\ \ \ | | |/ | |/| | | | | | | Conflicts: lib/cSig.mli
| * | Prevent coq_makefile from parsing project files in the reverse order. (Fix ↵Gravatar Guillaume Melquiond2016-01-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | Protect code against changes in Map interface.Gravatar Maxime Dénès2016-01-06
| | | | | | | | | | | | | | | | | | 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.
| * | Disable warning 31 when generating coqtop from coqmktop.Gravatar Maxime Dénès2016-01-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-05
|\ \ \
| | * | Avoid warning 31: test printer was linked twice with Dynlink and Str.Gravatar Maxime Dénès2016-01-05
| | | | | | | | | | | | | | | | | | | | Linking a module twice is unsafe and warning 31 will be fatal by default in OCaml 4.03. See PR#5461.
| | * | Fix order of files in mllib.Gravatar Maxime Dénès2016-01-05
| |/ / | | | | | | | | | | | | | | | | | | | | | 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 12:23:32 +0000