aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\
| * Fix previous commit.Gravatar Pierre-Marie Pédrot2016-10-17
| | | | | | | | I've messed up with parts of the compatibility files I had to commit.
| * Merge PR #300 into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
| |\
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\| |
| * | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
| |\ \
| * | | Little addition to 6eede071 for consistency of style in OrdersFacts.v.Gravatar Hugo Herbelin2016-10-12
| | | |
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-08
|\| | |
| * | | Fixing unexpected "noise" introduced in commit 24d5448c.Gravatar Hugo Herbelin2016-10-06
| | | | | | | | | | | | | | | | A file was introduced by mistake in theories/Logic.
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\| | |
| * | | Clean up type classes flags and update compat file.Gravatar Maxime Dénès2016-10-05
| | | |
| | * | Remove if_then_else. Use tryif instead.Gravatar Théo Zimmermann2016-10-03
| | | | | | | | | | | | | | | | | | | | if_then_else definition does not account for multi success tactics. tryif_then_else is a primitive tactical with the expected behavior.
| * | | More tests for tactic "subst".Gravatar Hugo Herbelin2016-10-02
| | | |
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\| | |
| | | * Move vector/list compat notations to their relevant filesGravatar Jason Gross2016-09-29
| | |/ | |/| | | | | | | | | | | | | | | | Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations no longer modify the parser in non-compat-mode, so we can do this without breaking Ltac parsing. Also update the related test-suite files.
| * | ZDivEucl: notations in different scope to avoid a warningGravatar Pierre Letouzey2016-09-28
| | |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-27
|\| |
| * | Remove spaces from around list notationsGravatar Jason Gross2016-09-26
| | |
| * | Remove spaces from around vector notationsGravatar Jason Gross2016-09-26
| | |
| * | Unbreak Ltac [ | .. | ] notation in -compat 8.5Gravatar Jason Gross2016-09-26
| | | | | | | | | | | | | | | | | | Importing VectorNotations breaks `; []`. So we make sure it's not imported by defualt. Some files might be required to `Import VectorDef.VectorNotations` rather than just `Import VectorNotations`.
| * | Fix bug #4785 (use [ ] for vector nil)Gravatar Jason Gross2016-09-26
| | | | | | | | | | | | | | | Also delimit vector_scope with vector, so that people can write %vector without having to delimit it themselves.
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\| |
* | | extensionality: Handle dependently-used hypothesesGravatar Jason Gross2016-09-19
| | |
* | | Adding an "extensionality in H" tactic which applies functionalGravatar Hugo Herbelin2016-09-19
| | | | | | | | | | | | | | | | | | | | | | | | extensionality in H supposed to be a quantified equality until giving a bare equality. Thanks to Jason Gross and Jonathan Leivent for suggestions and examples.
| * | Further "decide equality" tests on demand of Jason.Gravatar Hugo Herbelin2016-09-17
| | |
| * | Extending "contradiction" so that it recognizes statements such as "~x=x" or ↵Gravatar Hugo Herbelin2016-09-15
|/ / | | | | | | | | | | | | | | | | | | ~True. Found 1 incompatibility in tested contribs and 3 times the same pattern of incompatibility in the standard library. In all cases, it is an improvement in the form of the script. New behavior deactivated when version is <= 8.5.
* | Refolding: disable in 8.4 compat file, documentGravatar Matthieu Sozeau2016-09-12
| |
* | no-refold patchGravatar Paul Steckler2016-09-09
| | | | | | | | | | | | Add a boolean for refolding during reduction, and an option that is off by default in 8.6, to turn refolding on in all reduction functions, as in 8.5.
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-02
|\|
| * Fix bug #5043: [Admitted] lemmas pick up section variables.Gravatar Pierre-Marie Pédrot2016-08-31
| | | | | | | | | | | | We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables.
* | Merge remote-tracking branch 'origin/pr/246' into v8.6Gravatar Matthieu Sozeau2016-08-19
|\ \
* \ \ Merge remote-tracking branch 'github/bug4978' into v8.6Gravatar Matthieu Sozeau2016-08-18
|\ \ \
* | | | Fix an occurrence of deprecated eqn syntax in stdlib.Gravatar Maxime Dénès2016-08-18
| | | |
| * | | Fix #4978: priorities of Equivalence instancesGravatar Matthieu Sozeau2016-08-17
|/ / /
* | | Replacing deprecated Implicit Arguments in prelude.Gravatar Maxime Dénès2016-07-18
| | | | | | | | | | | | Was triggering a deprecation warning.
* | | Remove the swap tactic from the prelude.Gravatar Maxime Dénès2016-07-18
| | | | | | | | | | | | | | | It was anyway unusable due to a parsing conflict with the swap operator on goals. Was triggering a warning when compiling the prelude.
* | | Fix bug #4923: Warning: appcontext is deprecated.Gravatar Pierre-Marie Pédrot2016-07-18
| | |
| | * Typo.Gravatar Hugo Herbelin2016-07-13
| | |
* | | Typo in a comment of stdlib.Gravatar Hugo Herbelin2016-07-08
| | |
| * | Program: Move ProofIrrelevance to Subset.vGravatar Matthieu Sozeau2016-07-08
| | |
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\ \ \ | |/ / |/| / | |/
| * Merge remote-tracking branch 'github/pr/199' into v8.5Gravatar Maxime Dénès2016-07-06
| |\ | | | | | | | | | Was PR#199: Unbreak singleton list-like notation (-compat 8.4)
* | | Fix #4793: Coq 8.6 should accept -compat 8.6Gravatar Maxime Dénès2016-07-06
| | | | | | | | | | | | We also add a Coq86.v compat file.
| * | Move option_map notation upGravatar Jason Gross2016-07-05
| | | | | | | | | This way, it's not eaten by a section
| * | Restore option_map in FMapFactsGravatar Jason Gross2016-07-05
| | | | | | | | | This definition was removed by a4043608f704f026de7eb5167a109ca48e00c221 (This commit adds full universe polymorphism and fast projections to Coq), for reasons I do not know. This means that things like `unfold option_map` work only in 8.5, while `unfold <application of Facts>.option_map` works only in 8.4. This allows `unfold` to work correctly in both 8.4 and 8.5.
| | * Compat84: Don't mess with stdlib modulesGravatar Jason Gross2016-07-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | We don't actually need to, unless we want to support the (presumably uncommon) use-case of someone using [Import VectorNotations] to override their local notation for things in vector_scope. Additionally, we now maintain the behavior that [Import VectorNotations] opens vector_scope.
* | | Typeclasses: use once in by clause for typeclass eautoGravatar Matthieu Sozeau2016-06-28
| | | | | | | | | | | | | | | Otherwise we may backtrack on the resolution in a by which seems strange.
* | | Add Unset Shrink Abstract/Obligations in Coq85Gravatar Matthieu Sozeau2016-06-27
| | | | | | | | | | | | For compatibility with 8.5.
* | | Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There were three versions of injection: 1. "injection term" without "as" clause: was leaving hypotheses on the goal in reverse order 2. "injection term as ipat", first version: was introduction hypotheses using ipat in reverse order without checking that the number of ipat was the size of the injection (activated with "Unset Injection L2R Pattern Order") 3. "injection term as ipat", second version: was introduction hypotheses using ipat in left-to-right order checking that the number of ipat was the size of the injection and clearing the injecting term by default if an hypothesis (activated with "Set Injection L2R Pattern Order", default one from 8.5) There is now: 4. "injection term" without "as" clause, new version: introducing the components of the injection in the context in left-to-right order using default intro-patterns "?" and clearing the injecting term by default if an hypothesis (activated with "Set Structural Injection") The new versions 3. and 4. are the "expected" ones in the sense that they have the following good properties: - introduction in the context is in the natural left-to-right order - "injection" behaves the same with and without "as", always introducing the hypotheses in the goal what corresponds to the natural expectation as the changes I made in the proof scripts for adaptation confirm - clear the "injection" hypothesis when an hypothesis which is the natural expectation as the changes I made in the proof scripts for adaptation confirm The compatibility can be preserved by "Unset Structural Injection" or by calling "simple injection". The flag is currently off.
* | | Remove unneded hints in NZGcdGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | | | They were already commented out, Pierre confirms they're spurious.
* | | setoid_rewrite: fix the Params resolution tacticGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | | | | | | | | | Add a substitution of a local variable by its body to ensure proper unification without having to make all local variables unfoldable.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 11:19:48 +0000