aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Safer API for Global.body_of_constant and variants.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | We aditionally return the abstract universe context inside the option. This is relatively painless as most uses were using the option as a boolean.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Merge PR#843: closing bug #5618 introduce by PR 828Gravatar Maxime Dénès2017-06-30
|\
| * closing bug #5618 introduce by PR 828Gravatar Julien Forest2017-06-29
| |
* | Merge PR#828: closing bug #4250Gravatar Maxime Dénès2017-06-26
|\|
* | Merge PR#794: Cleanup of ltac cmxsGravatar Maxime Dénès2017-06-23
|\ \
| | * closing bug #4250Gravatar Julien Forest2017-06-23
| |/ |/|
* | Merge PR#807: romega: fix a slowdownGravatar Maxime Dénès2017-06-20
|\ \
* \ \ Merge PR#803: Clean ssrGravatar Maxime Dénès2017-06-20
|\ \ \
| | * | romega: avoid potential slowdown when changing concl by reified versionGravatar Pierre Letouzey2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On some benchmarks provided by Chantal Keller a long time ago, romega was abnormally slow compared to omega (or lia). It turned out that the change of concl by reified version was triggering unnecessary unfolds of Z.add, instead of unfolding ReflOmegaCore.Z_as_Int.plus into Z.add. This is now fixed by the various Parameter Inline : no more indirections, Z_as_Int.plus is directly Z.add. Also use Tactics.convert_concl_no_check for this "change", as recommended by PMP.
| * | | Removing Proof_type from the API.Gravatar Pierre-Marie Pédrot2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Unluckily, this forces replacing a lot of code in plugins, because the API defined the type of goals and tactics in Proof_type, and by the no-alias rule, this was the only one. But Proof_type was already implicitly deprecated, so that the API should have relied on Tacmach instead.
| * | | Remove the last use of the low-level Proof_type API in ssr.Gravatar Pierre-Marie Pédrot2017-06-16
| |/ /
* | | Fix bugs and add an option for cumulativityGravatar 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#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\ \
| | * plugins/ltac : avoid spurious .cmxs filesGravatar Pierre Letouzey2017-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs (for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus : - wrong -for-pack used for their inner .cmx - dependency over modules not provided (for instance Tacenv, that ends up being a submodule of the pack ltac_plugin). But we were lucky, those files were actually never loaded, thanks to the several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin, and hence tell Coq that these modules are already known, preventing any attempt to load them. Anyway, this commit cleans up this mess (thanks PMP for the help)
* | | Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \ \ | |_|/ |/| |
* | | 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
|\ \ \ \
* \ \ \ \ Merge PR#673: Two fixes about zify (bugs #5336 and #5439)Gravatar Maxime Dénès2017-06-14
|\ \ \ \ \
* \ \ \ \ \ Merge PR#622: Change the default flag value for Refine.refineGravatar Maxime Dénès2017-06-14
|\ \ \ \ \ \
* | | | | | | Recdef do now a Require Export FunInd (better compat)Gravatar Pierre Letouzey2017-06-14
| | | | | | |
* | | | | | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
* | | | | | | Makefile.build : cleanup now that micromega.ml isn't generated + sync check ↵Gravatar Pierre Letouzey2017-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | of this file There is now a warning if the content of micromega.ml isn't what MExtraction.v would produce.
| | | | | | * Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
| |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml
| | | | | * Deprecate options that were introduced for compatibility with 8.2.Gravatar Guillaume Melquiond2017-06-14
| | | | | |
| | | | | * Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
| |_|_|_|/ |/| | | |
| * | | | Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
| | | | |
| * | | | Explicit the unsafe flag of all calls to Refine.refine.Gravatar Pierre-Marie Pédrot2017-06-13
| | | | |
* | | | | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
|/ / / / | | | | | | | | | | | | | | | | | | | | See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude.
* | | | Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to ↵Gravatar Matej Košík2017-06-12
| | | | | | | | | | | | | | | | generate them later.
* | | | Merge PR#709: Bytecode compilation apart from 'make world', againGravatar Maxime Dénès2017-06-12
|\ \ \ \
* \ \ \ \ Merge PR#718: API cleanup: aliasesGravatar Maxime Dénès2017-06-12
|\ \ \ \ \
| | | * | | zify: force reduction of (Z.max 0 0) and similar (fix #5439)Gravatar Pierre Letouzey2017-06-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Turn some "simpl" into "compute". Also do the same for the few "simpl (Z.of_nat ...)". This way, definition like Z.max are properly reduced, and moreover zify isn't sensible anymore to the "Arguments Z.of_nat : simpl never" that some user want (see also #5039). Unfortunately, the compute we're using now still honor the "Opaque" declarations, so a "Opaque Z.max" will block things again (see also #5374).
| | | * | | zify: confusion between Pos2Z.inj_sub and Pos2Z.inj_sub_max (fix #5336)Gravatar Pierre Letouzey2017-06-12
| |_|/ / / |/| | | |
| | | | * [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`.
* | | | Remove remaining vo.itarget files (obsolete since PR #499)Gravatar Pierre Letouzey2017-06-10
| | | |
| * | | Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
| | | |
| | | * 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
|\ \ \ | |/ / |/| |
* | | Put "ssreflect" behind "API".Gravatar Matej Košík2017-06-07
| | |
* | | Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
| | |
* | | Merge the ssr plugin.Gravatar Maxime Dénès2017-06-06
| | |
* | | 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.
* | | Merge PR#600: Some factorizations of ltac interpretation functions between ↵Gravatar Maxime Dénès2017-06-06
|\ \ \ | | | | | | | | | | | | ssreflect and coq code
* \ \ \ Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\ \ \ \
* \ \ \ \ Merge PR#722: [printing] Remove duplicated printing function.Gravatar Maxime Dénès2017-06-05
|\ \ \ \ \
* \ \ \ \ \ Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ↵Gravatar Maxime Dénès2017-06-05
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | a flag suspectingly renamed in a clearer way
* \ \ \ \ \ \ Merge PR#526: solving implicit resolution in FunctionGravatar Maxime Dénès2017-06-04
|\ \ \ \ \ \ \
| | | | * | | | 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 ```
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 06:23:17 +0000