| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-03-10 | Primitive projections: protect kernel from erroneous definitions. | Matthieu Sozeau | |
| E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive records with eta for which conversion is incomplete. - Eta-conversion only applies to BiFinite inductives - Finiteness information is now checked by the kernel (the constructor types must be strictly non recursive for BiFinite declarations). | |||
| 2016-03-10 | Removing OCaml deprecated function names from the Lazy module. | Pierre-Marie Pédrot | |
| 2016-03-10 | Hashconsing modules. | Pierre-Marie Pédrot | |
| Modules inserted into the environment were not hashconsed, leading to an important redundancy, especially in module signatures that are always fully expanded. This patch divides by two the size and memory consumption of module-heavy files by hashconsing modules before putting them in the environment. Note that this is not a real hashconsing, in the sense that we only hashcons the inner terms contained in the modules, that are only mapped over. Compilation time should globally decrease, even though some files definining a lot of modules may see their compilation time increase. Some remaining overhead may persist, as for instance module inclusion is not hashconsed. | |||
| 2016-03-09 | Merge branch 'render-prehistory' of https://github.com/aspiwack/coq into ↵ | Hugo Herbelin | |
| aspiwack-render-prehistory3 Pull request #120 | |||
| 2016-03-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-03-09 | Fix test-suite file coq-prog-args | Matthieu Sozeau | |
| They were not parsed correctly with a newline in the middle. | |||
| 2016-03-09 | Redo fix init_setoid -> init_relation_classes | Matthieu Sozeau | |
| It got lost during a merge with the 8.5 branch. | |||
| 2016-03-09 | Fixed bug #4533 with previous Keyed Unification commit | Matthieu Sozeau | |
| Add test-suite file to ensure non-regression. | |||
| 2016-03-09 | Win: kill unreliable hence do not waitpid after kill -9 (Close #4369) | Enrico Tassi | |
| This commit also completes 74bd95d10b9f4cccb4bd5b855786c444492b201b | |||
| 2016-03-09 | Fix strategy of Keyed Unification | Matthieu Sozeau | |
| Try first to find a keyed subterm without conversion/betaiota on open terms (that is the usual strategy of rewrite), if this fails, try with full conversion, incuding betaiota. This makes the test-suite pass again, retaining efficiency in the most common cases. | |||
| 2016-03-07 | Adding backtraces to scheme error messages. | Pierre-Marie Pédrot | |
| 2016-03-07 | Re-enable OCaml warnings disabled by mistake as part of e759333. | Maxime Dénès | |
| 2016-03-06 | Partial disentangling of Ltac codebase. | Pierre-Marie Pédrot | |
| 2016-03-06 | Expurging grammar.mllib from uselessly linked modules. | Pierre-Marie Pédrot | |
| 2016-03-06 | Moving Autorewrite to Hightatctic. | Pierre-Marie Pédrot | |
| 2016-03-06 | Putting Tactic_debug just below Tacinterp. | Pierre-Marie Pédrot | |
| 2016-03-06 | Removing dependency of Himsg in tactic files. | Pierre-Marie Pédrot | |
| 2016-03-06 | Moving Tactic_debug to tactics/ folder. | Pierre-Marie Pédrot | |
| 2016-03-06 | Moving Ltac traces to Tacexpr and Tacinterp. | Pierre-Marie Pédrot | |
| 2016-03-06 | Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move. | Pierre-Marie Pédrot | |
| We just reuse the same one weird old trick in CAMLP4 to compare keywords and identifiers as tokens. Note though that the commit 982460743 does not fix the keyword vs. identifier issue in CAMLP4, so that the corresponding test fails. This means that since that commit, some code compiling with CAMLP5 does not when using CAMLP4, making it a second-class citizen. | |||
| 2016-03-06 | Removing useless grammar.cma dependencies. | Pierre-Marie Pédrot | |
| 2016-03-06 | Splitting the nsatz ML module into an implementation and a grammar files. | Pierre-Marie Pédrot | |
| 2016-03-06 | Moving Eauto to a simple ML file. | Pierre-Marie Pédrot | |
| 2016-03-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-03-05 | Using build_selector from Equality as a replacement of the selector | Hugo Herbelin | |
| in cctac which does not support indices properly. Incidentally, this should fix a failure in RelationAlgebra, where making prod_applist more robust (e8c47b652) revealed the discriminate bug in congruence. | |||
| 2016-03-05 | Exporting build_selector, a component of discriminate, for use in congruence. | Hugo Herbelin | |
| 2016-03-05 | Generalizing the uses of tactic scopes everywhere. | Pierre-Marie Pédrot | |
| This feature allows the user to write "let x := open_constr(foo) in ..." for instance without having to resort to tactic notations. Some changes have been introduced in the parsing of ad-hoc argument scopes, e.g. one has to put parentheses around constr:(...) and ltac:(...) in tactics. This breaks badly written scripts, although it is easy to be forward-compatible by preemptively putting thoses parentheses. | |||
| 2016-03-05 | Fixing bug #4608: Anomaly "output_value: abstract value (outside heap)". | Pierre-Marie Pédrot | |
| The ARGUMENT EXTEND statement was wrongly using a CompatLoc instead of a Loc, and this was not detected by typing "thanks" to the Gram.action magic. When using CAMLP4, this was wreaking havoc at runtime, but not when using CAMLP5, as the locations where sharing the same representation. | |||
| 2016-03-04 | Fix #4607: do not read native code files if native compiler was disabled. | Maxime Dénès | |
| 2016-03-04 | This fix is probably not enough to justify that there are no problems with | Maxime Dénès | |
| primitive projections and prop. ext. or univalence, but at least it prevents known proofs of false (see discussion on #4588). | |||
| 2016-03-04 | Adding some standard arguments in tactic scopes. | Pierre-Marie Pédrot | |
| This is not perfect and repeats what we do in Pcoq, but it is hard to factorize because rules defined in Pcoq do not have the same precedence. For instance, constr as a Tactic Notation argument is a Pcoq.Constr.constr while as a quotation argument is a Pcoq.Constr.lconstr. We should think of a fix in the long run, but for now it is reasonable to duplicate code. | |||
| 2016-03-04 | Rename Ephemeron -> CEphemeron. | Maxime Dénès | |
| Fixes compilation of Coq with OCaml 4.03 beta 1. | |||
| 2016-03-04 | All arguments defined through ARGUMENT EXTEND declare a tactic scope. | Pierre-Marie Pédrot | |
| Amongs other things, it kind of fixes bug #4492, even though you cannot really take advantage of the parsed data for now. | |||
| 2016-03-04 | Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations]. | Pierre-Marie Pédrot | |
| 2016-03-04 | Exchanging roles of tactic_arg and tactic_top_or_arg entries. | Pierre-Marie Pédrot | |
| The tactic_arg entry was essentially a hack to keep parsing constrs as tactic arguments. We rather use tactic_top_or_arg as the true entry for tactic arguments now. | |||
| 2016-03-04 | Removing the UConstr entry of the tactic_arg AST. | Pierre-Marie Pédrot | |
| This was redundant with the wit_uconstr generic argument, so there was no real point on keeping it there. | |||
| 2016-03-04 | Making parentheses mandatory in tactic scopes. | Pierre-Marie Pédrot | |
| 2016-03-04 | Uniformizing the parsing of argument scopes in Ltac. | Pierre-Marie Pédrot | |
| 2016-03-04 | Merge pull request #97 from clarus/trunk | Pierre-Marie Pédrot | |
| Converting the README to MarkDown syntax. | |||
| 2016-03-04 | Fix a typo in dev/doc/changes.txt | Jason Gross | |
| CQQ -> COQ | |||
| 2016-03-03 | Adding a test for the behaviour of open_constr described in #3777. | Pierre-Marie Pédrot | |
| 2016-03-03 | Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop. | Pierre-Marie Pédrot | |
| Printing invalid UTF-8 string startled GTK too much, leading to CoqIDE dying improperly. We now check that all strings outputed by Coq are proper UTF-8. This is not perfect, as CoqIDE will sometimes truncate strings which contains the null character, but at least it should not crash. | |||
| 2016-03-02 | Ssreflect pattern matching facilities | Enrico Tassi | |
| 2016-02-29 | Merge branch 'clean-atomic-tactics' | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "move" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "exists" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "symmetry" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "generalize dependent" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "clearbody" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "clear" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |