aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2016-05-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-04NPeano : improve compatibility for this deprecated file via compat notationsPierre Letouzey
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-04Int.v: simplify Jason's commit 5b4e3acePierre Letouzey
2016-05-04Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq ↵Pierre Letouzey
into v8.5
2016-05-02Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-27Revert "Changing rule for "*" in Operator_Properties so that, iterated, it"Hugo Herbelin
This reverts commit c4d1e3113f77af2e5474fe5676c272050dd445e5.
2016-04-27Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"Hugo Herbelin
This reverts commit 5bed8869b90510f719dcaa5e365b81c6309bdfff.
2016-04-27Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ↵Hugo Herbelin
the levels." This reverts commit b6db76517b9a7f21078ab59a0b8eeee6bfdf5ba7.
2016-04-27Revert "Temporary hack to compensate missing comma while re-printing tactic"Hugo Herbelin
This reverts commit 3a2753bedf43a8c7306b1b3fc9cb37aafb78ad7a.
2016-04-27Temporary hack to compensate missing comma while re-printing tacticHugo Herbelin
"exists c1, c2".
2016-04-27In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.Hugo Herbelin
2016-04-27Adding option "Set Reversible Pattern Implicit" to Specif.v so that anHugo Herbelin
implicit is found whether one writes (sig P) or {x|P x}.
2016-04-27Changing rule for "*" in Operator_Properties so that, iterated, itHugo Herbelin
does not print to ** which is a keyword.
2016-04-25Fixing bug #4684: Singleton list notation unusable in 8.5pl1.Pierre-Marie Pédrot
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-08Added compatibility coercions from Specif.v which were present in Coq 8.4.Hugo Herbelin
2016-04-05Add -compat 8.4 econstructor tactics, and testsJason Gross
Passing `-compat 8.4` now allows the use of `econstructor (tac)`, as in 8.4.
2016-04-05Fix bug #4656Jason Gross
I introduced this bug in 4c078b0362542908eb2fe1d63f0d867b339953fd; Coq.Init.Notations.constructor does not take any arguments.
2016-04-04Update Coq84.vJason Gross
We no longer need to redefine `refine` (it now shelves by default). Also clean up `constructor` a bit.
2016-04-04Add compatibility Nonrecursive Elimination SchemesJason Gross
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵Matthieu Sozeau
into JasonGross-trunk-function_scope
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-24Fix handling of arity of definitional classes.Matthieu Sozeau
The user-provided sort was ignored for them.
2016-03-06Moving Eauto to a simple ML file.Pierre-Marie Pédrot
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-02-26Qcabs : absolute value on normalized rational numbers QcPierre Letouzey
File contributed by Cédric Auger (a long time ago, sorry!) Qarith and Qc would probably deserve many more results like this one, and a more modern style (for instance qualified names), but this commit is better than nothing...
2016-02-26Qcanon : fix names of lemmas Qcle_alt & Qcge_alt (were Qle_alt & Qge_alt)Pierre Letouzey
2016-02-26Qcanon : implement some old suggestions by C. AugerPierre Letouzey
2016-02-23Moving tauto.ml4 to a proper ML file.Pierre-Marie Pédrot
2016-02-22Moving the Tauto tactic to proper Ltac.Pierre-Marie Pédrot
This gets rid of brittle code written in ML files through Ltac quotations, and reduces the dependance of Coq to such a feature. This also fixes the particular instance of bug #2800, although the underlying issue is still there.
2016-02-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-19Fixing bug #4582: cannot override notation [ x ].Pierre-Marie Pédrot
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-23Fix bug #4503: mixing universe polymorphic and monomorphicMatthieu Sozeau
variables and definitions in sections is unsupported.
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-21Stronger invariants on the use of the introduction pattern (pat1,...,patn).Hugo Herbelin
The length of the pattern should now be exactly the number of assumptions and definitions introduced by the destruction or induction, including the induction hypotheses in case of an induction. Like for pattern-matching, the local definitions in the argument of the constructor can be skipped in which case a name is automatically created for these.
2016-01-20Update copyright headers.Maxime Dénès
2016-01-13MMaps: remove it from final 8.5 release, since this new library isn't mature ↵Pierre Letouzey
enough In particular, its interface might still change (in interaction with interested colleagues). So let's not give it too much visibility yet. Instead, I'll turn it as an opam packages for now.
2016-01-05Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2015-12-31Put implicits back as in 8.4.Matthieu Sozeau
2015-12-29Move compatibility notations to their proper filesJason Gross
2015-12-24Removing auto from the tactic AST.Pierre-Marie Pédrot
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-15Proof using: do not clear unused section hyps automaticallyEnrico Tassi
The option is still there, but not documented since it is too dangerous. Hints and type classes instances are not taking cleared variables into account.
2015-12-15Refine tactic now shelves unifiable holes.Pierre-Marie Pédrot
The unshelve tactical can be used to get the shelved holes. This changes the proper ordering of holes though, so expect some broken scripts. Also, the test-suite is not fixed yet.
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-14Moved proof_admitted to its own file, named "AdmitAxiom.v".Maxime Dénès
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-10Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Hugo Herbelin
Marking it as experimental.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 04:10:18 +0000