aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Collapse)AuthorAge
...
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
| | | | | | | | | | | | | | Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions.
* Fix a refine anomaly "Evar defined twice".Gravatar Pierre-Marie Pédrot2017-09-06
| | | | | | Because the argument given to refine may mess with the evarmap, the goal being refined can be solved by side-effect after the term filler is computed. If this happens, we simply don't perform the refining operation.
* Merge PR #946: Functional pretyping interfaceGravatar Maxime Dénès2017-08-29
|\
* \ Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\ \
| | * Move glob_constr_ltac_closure to evar_refiner.Gravatar Maxime Dénès2017-08-01
| |/ |/|
* | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \
| * | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | |
* | | Statically ensuring that inlined entries out of the kernel have no effects.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | | | | | This was an easy to prove property that I somehow overlooked.
* | | More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
|/ / | | | | | | | | We use an algebraic type instead of a pair of a boolean and the corresponding data. For now, this is isomorphic, but this allows later change in the structure.
* | [api] Put modules in order in API.{mli,ml}Gravatar Emilio Jesus Gallego Arias2017-07-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We sort the dependency graph of API by following a logical declaration order in `API.{ml,mli}` related to the actual dependency order of Coq modules. Things are a bit tricky here as Coq itself relies on the fact that OCaml treats module interface and implementation separately dependency-wise; however, when resorting module alias the design seems to become more coupled. Currently, API exposes both "namespaces", asserting a large number of type equality between them, however the `API` namespace is not self-contained. In particular, this is a first step to solve problems such as `Summary.frozen` being used in `API.mli` but not declared by the `API.Summary` module, etc... In general we follow the invariant that a type used in `API` must have been declared before. Keep in mind that OCaml upstream has warned that it maybe tricky to alias objects in this way. In particular, after API the old `mli` only files have become full compilation units so we may want to be more careful here. The more "correct" declaration order allows us to remove the `API.Prelude` module, as well as some other declarations that I consider as spurious. We still maintain the large number of type aliases which will be removed in a future patch. We follow linking order except for files in `intf`, which are conceptually wrongly placed in the linking hierarchy but this doesn't matter as the files don't contain any implementation. We also move a couple of `.mli` only files to `.ml` so we are consistent, and correct their linking order in `mllib`, even if that doesn't matter as such `.ml`-only files contain no implementations.
* | Merge PR #899: [general] Move files to directories so they match linking order.Gravatar Maxime Dénès2017-07-20
|\ \
* \ \ Merge PR #770: [proof] Move bullets to their own module.Gravatar Maxime Dénès2017-07-19
|\ \ \
| | * | [general] Move files to directories matching linking order.Gravatar Emilio Jesus Gallego Arias2017-07-19
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`, `Miscprint`) to their proper place as they were declared in different `mllib` files than the one in their directory. In some cases this could be refined but we don't do anything fancy, we just reflect the status quo.
* | | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| | |
| | * Moving "assert" (internally "Cut") to the new proof engine.Gravatar Hugo Herbelin2017-06-25
| | | | | | | | | | | | | | | It allows in particular to have "Info" on tactic "assert" and derivatives not to give an "<unknown>".
| | * Exporting general-purpose functions on goal contexts from "logic.ml" to ↵Gravatar Hugo Herbelin2017-06-25
| |/ |/| | | | | | | | | "tactics.ml". This is in preparation of move of "assert" from old to new proof engine.
* | Merge PR#777: Improving documentation of tactic "move" (report #4561)Gravatar Maxime Dénès2017-06-19
|\ \
* | | Remove Warnings: unused value ...Gravatar Amin Timany2017-06-16
| | |
* | | Squashed commit of the following:Gravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Except I have disabled the minimization of universes after sections as it seems to interfere with the STM machinery causing files like test-suite/vio/print.v to loop when processed asynchronously. This is very peculiar and needs more investigation as the aforementioned file does not have any sections or any universe polymorphic definitions! commit fc785326080b9451eb4700b16ccd3f7df214e0ed Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:14:21 2017 +0200 Revert STL to monomorphic commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996 Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:02:42 2017 +0200 Try unifying universes before apply subtyping commit ff393742c37b9241c83498e84c2274967a1a58dc Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 23 13:49:04 2017 +0200 Compile more of STL with universe polymorphism commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6 Author: Amin Timany <amintimany@gmail.com> Date: Tue Apr 18 21:26:45 2017 +0200 Made more progress on compiling the standard library commit b8550ffcce0861794116eb3b12b84e1158c2b4f8 Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 16 22:55:19 2017 +0200 Make more number theoretic modules monomorphic commit 29d126d4d4910683f7e6aada2a25209151e41b10 Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 16:11:48 2017 +0200 WIP more of standard library compiles Also: Matthieu fixed a bug in rewrite system which was faulty when introducing new morphisms (Add Morphism) command. commit 23bc33b843f098acaba4c63c71c68f79c4641f8c Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 11:39:21 2017 +0200 WIP: more of the standard library compiles We have implemented convertibility of constructors up-to mutual subtyping of their corresponding inductive types. This is similar to the behavior of template polymorphism. commit d0abc5c50d593404fb41b98d588c3843382afd4f Author: Amin Timany <amintimany@gmail.com> Date: Wed Apr 12 19:02:39 2017 +0200 WIP: trying to get the standard library compile with universe polymorphism We are trying to prune universes after section ends. Sections add a load of universes that are not appearing in the body, type or the constraints.
* | | Merge PR#763: [proof] Deprecate redundant wrappers.Gravatar Maxime Dénès2017-06-14
|\ \ \
* \ \ \ Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \ \ \
| | | * | Improving documentation of tactic "move" (report #4561).Gravatar Hugo Herbelin2017-06-13
| | | | |
* | | | | Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
| | | | |
* | | | | Turn the default behaviour of the refine primitive into the safe one.Gravatar Pierre-Marie Pédrot2017-06-13
| |_|/ / |/| | |
| | | * [proof] Move bullets to their own module.Gravatar Emilio Jesus Gallego Arias2017-06-12
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | Bullets were placed inside the `Proof_global` module, I guess that due to the global registration function. However, it has logically nothing to do with the functionality of `Proof_global` and the current placement may create some interference between the developers reworking proof state handling and bullets. We thus put the bullet functionality into its own, independent file.
| | * [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
| |/ |/| | | | | | | | | | | | | | | As we would like to reduce the role of proof_global in future versions, we start to deprecate old compatibility aliases in `Pfedit` in favor of the real functions underlying the 8.5 proof engine. We also deprecate a couple of alias types and explicitly mark the few remaining uses of `Pfedit`.
| * A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
|/ | | | | | | | | Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let".
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\
* \ Merge PR#717: [proof] Deprecate "proof mode" APIGravatar Maxime Dénès2017-06-07
|\ \
* | | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Reminder of (some of) the reasons for removal: - Despite the claim in sigma.mli, it does *not* prevent evar leaks, something like: fun env evd -> let (evd',ev) = new_evar env evd in (evd,ev) will typecheck even with Sigma-like type annotations (with a proof of reflexivity) - The API stayed embryonic. Even typing functions were not ported to Sigma. - Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly less unsafe ones (e.g. s_enter), but those ones were not marked unsafe at all (despite still being so). - There was no good story for higher order functions manipulating evar maps. Without higher order, one can most of the time get away with reusing the same name for the updated evar map. - Most of the code doing complex things with evar maps was using unsafe casts to sigma. This code should be fixed, but this is an orthogonal issue. Of course, this was showing a nice and elegant use of GADTs, but the cost/benefit ratio in practice did not seem good.
* | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
* | | Don't double up on periods in anomaliesGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | | | | | | | | We don't want "Anomaly: Returned a functional value in a type not recognized as a product type.. Please report at http://coq.inria.fr/bugs/." but instead "Anomaly: Returned a functional value in a type not recognized as a product type. Please report at http://coq.inria.fr/bugs/."
* | | Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Maxime Dénès2017-06-02
|\ \ \
| * | | [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
| | | | | | | | | | | | | | | | | | | | We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel.
* | | | Merge PR#696: Trunk+cleanup constr of globalGravatar Maxime Dénès2017-06-01
|\ \ \ \
| | | * | [proof] Deprecate "proof mode" APIGravatar Emilio Jesus Gallego Arias2017-05-31
| | |/ / | | | | | | | | | | | | | | | | Any users of this API should coordinate with the ongoing work in PRs numbered #459 and #566.
* | / / Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This module collects the functions of Nameops which are about Name.t and somehow standardize or improve their name, resulting in particular from discussions in working group. Note the use of a dedicated exception rather than a failwith for Nameops.Name.out. Drawback of the approach: one needs to open Nameops, or to use long prefix Nameops.Name.
| * | Cleanup: removal of constr_of_global.Gravatar Matthieu Sozeau2017-05-29
|/ / | | | | | | | | | | Constrintern.pf_global returns a global_reference, not a constr, adapt plugins accordingly, properly registering universes where necessary.
* | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | | | | | | | | | | | | | | | | | | | This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
* | Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\ \
* \ \ Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \ \
* \ \ \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \ \
| | * | | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
| * | | | Merge PR#642: Small cleanup on `close_proof` type.Gravatar Maxime Dénès2017-05-24
| |\ \ \ \ | | |/ / / | |/| | |
| | | | * Fix bindings handling of setoid_rewrite.Gravatar Cyprien Mangin2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | This fixes the discrepancy between "rewrite H with (1 := x)" and "setoid_rewrite H with (1 := x)".
| | * | | [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We'd like to cleanup the `proof_end` type so we can have a smaller path in proof save. Note that the construction: ``` Goal Type. ⋮ Save id. ``` has to be handled by the STM in the same path as Defined (but with an opaque flag), as `Save id` will alter the environment and cannot be processed in parallel. We thus try to simply such paths a bit, as complexity of `lemmas.ml` seems like an issue these days. The form `Save Theorem id` doesn't really seem used, and moreover we should really add a type of "Goal", and unify syntax. It is often the case that beginners try `Goal addnC n : n + 0 = n." etc...
| * | | | Change wrong bullet message.Gravatar Théo Zimmermann2017-05-20
| |/ / / | | | | | | | | | | | | | | | | | | | | Remove a space before colon. Remove the use of term mandatory (this closes https://coq.inria.fr/bugs/show_bug.cgi?id=3994).
| | * | Removing unused warnings.Gravatar Pierre-Marie Pédrot2017-05-19
| | | |
| | * | Generalizing the refine primitive so as to accept tactic arguments.Gravatar Pierre-Marie Pédrot2017-05-03
| |/ /
| * | Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
| |\ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 10:55:15 +0000