aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).Gravatar Maxime Dénès2017-08-01
|\
* \ Merge PR #919: Remove a few useless evar-normalizations in printing code.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
|\ \ \
* \ \ \ Merge PR #888: Stronger kernel typesGravatar Maxime Dénès2017-07-28
|\ \ \ \
| | | | * Fixing bug #5671 (specialize unclean wrt Metas).Gravatar Hugo Herbelin2017-07-27
| |_|_|/ |/| | |
| | * | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | | |
| | | * Remove a few useless evar-normalizations in printing code.Gravatar Pierre-Marie Pédrot2017-07-26
| |_|/ |/| |
| * | 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.
* | Merge PR #868: Fix debug trace of typeclasses eauto.Gravatar Maxime Dénès2017-07-26
|\ \ | |/ |/|
* | Merge PR #892: Improve do_split option of typeclass resolutionGravatar Maxime Dénès2017-07-20
|\ \
* \ \ Merge PR #899: [general] Move files to directories so they match linking order.Gravatar Maxime Dénès2017-07-20
|\ \ \
* \ \ \ Merge PR #869: Enforce alternating separators in typeclass debug outputGravatar Maxime Dénès2017-07-20
|\ \ \ \
* \ \ \ \ Merge branch 'v8.7'Gravatar Maxime Dénès2017-07-20
|\ \ \ \ \
| | | * | | [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.
| | | | * Fix debug trace of typeclasses eauto.Gravatar Théo Zimmermann2017-07-19
| |_|_|/ |/| | |
| | | * Improve do_split option of typeclass resolutionGravatar Matthieu Sozeau2017-07-18
| |_|/ |/| | | | | | | | | | | It used to compute the dependencies of all undefined evars of the evar_map, while only the dependencies of resolvable evars are necessary.
* | | Getting rid of abstraction breaking code in tclABSTRACT.Gravatar Pierre-Marie Pédrot2017-07-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is probably the hardest case of them all, because tclABSTRACT fundamentally relies on the names of universes from the constant instance being the same as the one in the current goal. Adding to that the fact that the kernel is doing strange things when provided with a polymorphic definition with body universe constraints, it turns out to be a hellish nightmare to handle properly. At some point we need to clarifiy this in the kernel as well, although we leave it for some other patch.
* | | Remove the function Global.type_of_global_unsafe.Gravatar Pierre-Marie Pédrot2017-07-13
| | |
* | | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Gravatar Pierre-Marie Pédrot2017-07-13
| | |
* | | Getting rid of AUContext abstraction breakers in Elimschemes.Gravatar Pierre-Marie Pédrot2017-07-13
| | |
| | * format pairs of items for pr_depth to get alternating separatorsGravatar Paul Steckler2017-07-12
| | | | | | | | | | | | | | | eval thunks once in prlist_sep_lastsep, make code clearer add typeclass debug output test
| * | Backtracking on deprecation of Bracketing Last Intro Pattern.Gravatar Théo Zimmermann2017-07-11
| | | | | | | | | | | | | | | | | | As per @JasonGross's request who described a use case for this option in https://coq.inria.fr/bugs/show_bug.cgi?id=5633 and pending an alternative solution for this use case.
| * | Deprecate options that were introduced for compatibility with 8.5.Gravatar Théo Zimmermann2017-07-11
| |/
* / Safe API for accessing universe constraints of global references.Gravatar Pierre-Marie Pédrot2017-07-11
|/ | | | | | Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topologicalGravatar Maxime Dénès2017-06-19
|\
* \ Merge PR#613: Cumulativity for inductive typesGravatar Maxime Dénès2017-06-19
|\ \
* \ \ Merge PR#727: [tactics] Fix summary registration of global hint variable.Gravatar Maxime Dénès2017-06-19
|\ \ \
| | * | Clean up universes of constants and inductivesGravatar 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#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \ \
* \ \ \ Merge PR#763: [proof] Deprecate redundant wrappers.Gravatar Maxime Dénès2017-06-14
|\ \ \ \
| | | | * [typeclasses eauto] Fix bug #3943: non-termination in topologicalGravatar Matthieu Sozeau2017-06-14
| | | | | | | | | | | | | | | | | | | | sorting for the dependency order option.
| | * | | Deprecate options that were introduced for compatibility with 8.4.Gravatar Guillaume Melquiond2017-06-14
| | | | |
| | * | | Deprecate options that were introduced for compatibility with 8.2.Gravatar Guillaume Melquiond2017-06-14
| | | | |
| | * | | Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| | | | |
| | * | | Remove support for Coq 8.3.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
| |/ / |/| |
| * | [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`.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \
* | | 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#638: Fix bug #5360: anomalies in typeclass resolution outputGravatar Maxime Dénès2017-06-06
|\ \ \
* \ \ \ Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\ \ \ \
* \ \ \ \ 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
| | | | | * [tactics] Fix summary registration of global hint variable.Gravatar Emilio Jesus Gallego Arias2017-06-03
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | It looks like `Class_tactics` forgot to register a couple of global variables with the summary, thus creating problems on backtracking. Fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5578
| | * | | 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 ```
* | | | Merge PR#449: make specialize smarter (bug 5370).Gravatar Maxime Dénès2017-06-01
|\ \ \ \
* \ \ \ \ Merge PR#696: Trunk+cleanup constr of globalGravatar Maxime Dénès2017-06-01
|\ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 07:49:05 +0000