aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-03-14Try eta-expansion of records only on non-recursive onesMatthieu Sozeau
2016-03-13Adopting the same rules for interpreting @, abbreviations andHugo Herbelin
notations in patterns than in terms, wrt implicit arguments and scopes. See file Notations2.v for the conventions in use in terms. Somehow this could be put in 8.5 since it puts in agreement the interpretation of abbreviations and notations in "symmetric patterns" to what is done in terms (even though the interpretation rules for terms are a bit ad hoc). There is one exception: in terms, "(foo args) args'" deactivates the implicit arguments and scopes in args'. This is a bit complicated to implement in patterns so the syntax is not supported (and anyway, this convention is a bit questionable).
2016-03-13Adding a few functions on type union.Hugo Herbelin
2016-03-13Adding a file summarizing the inconsistencies in interpreting implicitHugo Herbelin
arguments and scopes with abbreviations and notations. Comments are welcome on the proposed solutions for uniformization.
2016-03-13Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Hugo Herbelin
2016-03-12A more explicit name to the asymmetric boolean flag.Hugo Herbelin
2016-03-12Removing an empty file detected by Luc Grateau.Hugo Herbelin
2016-03-10Removing OCaml deprecated function names from the Lazy module.Pierre-Marie Pédrot
2016-03-09Merge branch 'render-prehistory' of https://github.com/aspiwack/coq into ↵Hugo Herbelin
aspiwack-render-prehistory3 Pull request #120
2016-03-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-09Fix test-suite file coq-prog-argsMatthieu Sozeau
They were not parsed correctly with a newline in the middle.
2016-03-09Redo fix init_setoid -> init_relation_classesMatthieu Sozeau
It got lost during a merge with the 8.5 branch.
2016-03-09Fixed bug #4533 with previous Keyed Unification commitMatthieu Sozeau
Add test-suite file to ensure non-regression.
2016-03-09Win: kill unreliable hence do not waitpid after kill -9 (Close #4369)Enrico Tassi
This commit also completes 74bd95d10b9f4cccb4bd5b855786c444492b201b
2016-03-09Fix strategy of Keyed UnificationMatthieu 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-07Adding backtraces to scheme error messages.Pierre-Marie Pédrot
2016-03-07Re-enable OCaml warnings disabled by mistake as part of e759333.Maxime Dénès
2016-03-06Partial disentangling of Ltac codebase.Pierre-Marie Pédrot
2016-03-06Expurging grammar.mllib from uselessly linked modules.Pierre-Marie Pédrot
2016-03-06Moving Autorewrite to Hightatctic.Pierre-Marie Pédrot
2016-03-06Putting Tactic_debug just below Tacinterp.Pierre-Marie Pédrot
2016-03-06Removing dependency of Himsg in tactic files.Pierre-Marie Pédrot
2016-03-06Moving Tactic_debug to tactics/ folder.Pierre-Marie Pédrot
2016-03-06Moving Ltac traces to Tacexpr and Tacinterp.Pierre-Marie Pédrot
2016-03-06Fixing 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-06Removing useless grammar.cma dependencies.Pierre-Marie Pédrot
2016-03-06Splitting the nsatz ML module into an implementation and a grammar files.Pierre-Marie Pédrot
2016-03-06Moving Eauto to a simple ML file.Pierre-Marie Pédrot
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-05Using build_selector from Equality as a replacement of the selectorHugo 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-05Exporting build_selector, a component of discriminate, for use in congruence.Hugo Herbelin
2016-03-05Generalizing 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-05Fixing 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-04Fix #4607: do not read native code files if native compiler was disabled.Maxime Dénès
2016-03-04This fix is probably not enough to justify that there are no problems withMaxime 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-04Adding 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-04Rename Ephemeron -> CEphemeron.Maxime Dénès
Fixes compilation of Coq with OCaml 4.03 beta 1.
2016-03-04All 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-04Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].Pierre-Marie Pédrot
2016-03-04Exchanging 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-04Removing 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-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-03-04Uniformizing the parsing of argument scopes in Ltac.Pierre-Marie Pédrot
2016-03-04Merge pull request #97 from clarus/trunkPierre-Marie Pédrot
Converting the README to MarkDown syntax.
2016-03-04Fix a typo in dev/doc/changes.txtJason Gross
CQQ -> COQ
2016-03-03Adding a test for the behaviour of open_constr described in #3777.Pierre-Marie Pédrot
2016-03-03Fixing 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-02-29Merge branch 'clean-atomic-tactics'Pierre-Marie Pédrot
2016-02-29Moving the "move" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "exists" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 19:08:10 +0000