aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init
Commit message (Collapse)AuthorAge
...
* Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
|\
* \ Merge PR#605: Report a useful error for dependent inductionGravatar Maxime Dénès2017-05-05
|\ \
* \ \ Merge PR#593: Functional choice <-> [inhabited] and [forall] commuteGravatar Maxime Dénès2017-05-05
|\ \ \
| | * | Report a useful error for dependent inductionGravatar Tej Chajed2017-05-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The dependent induction tactic notation is in the standard library but not loaded by default, leading to a parser error message that is confusing and unhelpful. This commit adds a notation for dependent induction to Init that fails and reports [Require Import Coq.Program.Equality.] is required to use [dependent induction].
| * | | Functional choice <-> [inhabited] and [forall] commuteGravatar Gaetan Gilbert2017-04-30
| |/ /
* / / Add .dir-locals.el and _CoqProject files for emacs stdlib editingGravatar Jason Gross2017-04-28
|/ / | | | | | | | | | | | | | | | | | | | | | | These set up PG to use the local coqtop, and the local coqlib, when editing files in the stdlib. As per https://github.com/coq/coq/pull/386#issuecomment-279012238, we can use `_CoqProject` for `theories/Init`, and this allows CoqIDE to edit those files. However, we cannot use it for `theories/`, because a `_CoqProject` file will override a `.dir-locals.el` in the same directory, and there is no way to get PG to pick up a valid `-coqlib` from `_CoqProject` (because it'll take the path relative to the current directory, not relative to the directory of `_CoqProject`).
* | Merge PR#584: Give andb_prop a simpler proofGravatar Maxime Dénès2017-04-27
|\ \
* | | Small typo in commentGravatar Vadim Zaliva2017-04-26
| | |
| | * Add transparent_abstract tacticGravatar Jason Gross2017-04-25
| |/ |/|
| * Give andb_prop a simpler proofGravatar Jason Gross2017-04-25
|/ | | No need to use `discriminate`. This is the hopefully uncontroversial part of https://github.com/coq/coq/pull/401.
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\
* \ Merge PR#455: Farewell decl_modeGravatar Maxime Dénès2017-04-06
|\ \
| | * Merge branch 'origin/v8.5' into v8.6.Gravatar Hugo Herbelin2017-04-06
| | |\ | | | | | | | | | | | | Was needed to be done for a while.
* | | \ Merge PR#442: Allow interactive editing of Coq.Init.LogicGravatar Maxime Dénès2017-03-17
|\ \ \ \
* \ \ \ \ Merge PR#451: Add η principles for sigma typesGravatar Maxime Dénès2017-03-17
|\ \ \ \ \
| | | * | | Farewell decl_modeGravatar Enrico Tassi2017-03-07
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests.
* | | | | A couple of other useful properties about compare_cont.Gravatar Hugo Herbelin2017-03-03
| | | | | | | | | | | | | | | | | | | | | | | | | Don't know if compare_cont is very useful to use, but, at least, these extensions make sense.
* | | | | Compatibility of iff wrt not and imp.Gravatar Hugo Herbelin2017-03-03
| | | | | | | | | | | | | | | | | | | | This completes the series and cannot hurt.
| * | | | Add η principles for sigma typesGravatar Jason Gross2017-03-01
| | | | |
| * | | | Remove some trailing whitespace in Init/Specif.vGravatar Jason Gross2017-03-01
|/ / / /
| | | * Fixing a little bug in printing ex2 (type was printed "_" by default).Gravatar Hugo Herbelin2017-02-23
| | | |
| * | | Allow interactive editing of Coq.Init.LogicGravatar Jason Gross2017-02-21
|/ / / | | | | | | | | | | | | Without this change, coqtop complains that I need to require Coq.Init.Logic to use [replace ... with ... by ...].
* / / Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
|/ / | | | | | | | | | | | | This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.
* | Remove v62 from stdlib.Gravatar Théo Zimmermann2016-10-24
| | | | | | | | | | This old compatibility hint database can be safely removed now that coq-contribs do not depend on it anymore.
* | 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.
* | 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.
* | Adding option "Set Reversible Pattern Implicit" to Specif.v so that anGravatar Hugo Herbelin2016-06-16
| | | | | | | | implicit is found whether one writes (sig P) or {x|P x}.
* | Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 5bed8869b90510f719dcaa5e365b81c6309bdfff.
* | Adding option "Set Reversible Pattern Implicit" to Specif.v so that anGravatar Hugo Herbelin2016-04-27
| | | | | | | | implicit is found whether one writes (sig P) or {x|P x}.
* | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵Gravatar Matthieu Sozeau2016-04-04
|\ \ | | | | | | | | | into JasonGross-trunk-function_scope
* | | Moving Eauto to a simple ML file.Gravatar Pierre-Marie Pédrot2016-03-06
| | |
* | | Moving tauto.ml4 to a proper ML file.Gravatar Pierre-Marie Pédrot2016-02-23
| | |
* | | Moving the Tauto tactic to proper Ltac.Gravatar Pierre-Marie Pédrot2016-02-22
| | | | | | | | | | | | | | | | | | 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.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \ \ | | |/ | |/|
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
| | |
* | | Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
| | |
| * | Remove Print Universe directive.Gravatar Matthieu Sozeau2015-10-02
| | |
| * | Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
| | |
| | * Move type_scope into user space, fix some output logsGravatar Jason Gross2015-08-14
| | |
| | * Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Gravatar Jason Gross2015-08-14
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change in the semantics of arguments scopes: scopes can no longer be bound to Funclass or Sortclass (this does not seem to be useful)). It is useful to have function_scope for, e.g., function composition. This allows users to, e.g., automatically interpret ∘ as morphism composition when expecting a morphism of categories, as functor composition when expecting a functor, and as function composition when expecting a function. Additionally, it is nicer to have fewer special cases in the OCaml code, and give more things a uniform syntax. (The scope type_scope should not be special-cased; this change is coming up next.) Also explicitly define [function_scope] in theories/Init/Notations.v. This closes bug #3080, Build a [function_scope] like [type_scope], or allow [Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass] We now mention Funclass and Sortclass in the documentation of [Bind Scope] again.
| * Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Sorry so much. Reverted: 707bfd5719b76d131152a258d49740165fbafe03. 164637cc3a4e8895ed4ec420e300bd692d3e7812. b9c96c601a8366b75ee8b76d3184ee57379e2620. 21e41af41b52914469885f40155702f325d5c786. 7532f3243ba585f21a8f594d3dc788e38dfa2cb8. 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd. fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c. d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962. 6737055d165c91904fc04534bee6b9c05c0235b1. 342fed039e53f00ff8758513149f8d41fa3a2e99. 21525bae8801d98ff2f1b52217d7603505ada2d2. b78d86d50727af61e0c4417cf2ef12cbfc73239d. 979de570714d340aaab7a6e99e08d46aa616e7da. f556da10a117396c2c796f6915321b67849f65cd. d8226295e6237a43de33475f798c3c8ac6ac4866. fdab811e58094accc02875c1f83e6476f4598d26.
| * Adding a notation { x & P } for { x : _ & P }.Gravatar Hugo Herbelin2015-08-02
| |
* | Tentatively setting cons and Some with 1st implicit argument maximalGravatar Hugo Herbelin2015-05-09
|/ | | | (see #3695).
* Fix various typos in documentationGravatar Matěj Grabovský2015-03-31
| | | | Closes #57.
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
| | | | | | | | | | | | | | | - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
* Reorder the steps of the easy tactic. (Fix for bug #2630)Gravatar Guillaume Melquiond2015-02-25
| | | | | | | Due to the way it was laid out, the tactic could prove neither (Zle x x) nor (P /\ Q -> P) nor (P |- P /\ True) yet it could prove (Zle x x /\ True) and (P /\ Q |- P).
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
| | | | | | | | | | definitions. Instead of failing with an anomaly when trying to do conversion or computation with the vm's, consider polymorphic constants as being opaque and keep instances around. This way the code is still correct but (obviously) incomplete for polymorphic definitions and we avoid introducing an anomaly. The patch does nothing clever, it only keeps around instances with constants/inductives and compile constant bodies only for non-polymorphic definitions.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Improving elimination with indices, getting rid of intrusive residualGravatar Hugo Herbelin2014-11-02
| | | | local definitions...
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 13:12:41 +0000