aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
Commit message (Collapse)AuthorAge
...
| | * [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
| |/ |/| | | | | | | | | | | | | | | Today, both modes are controlled by a single flag, however this is a bit misleading as is_silent really means "quiet", that is to say `coqc -q` whereas "verbose" is Coq normal operation. We also restore proper behavior of goal printing in coqtop on quiet mode, thanks to @Matafou for the report.
* | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵Gravatar Maxime Dénès2017-04-12
|\ \ | | | | | | | | | record fields.
* \ \ Merge PR#379: Introducing evar-insensitive constrsGravatar Maxime Dénès2017-04-11
|\ \ \
* | | | [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
| | | * end of correction of bug 4306Gravatar Julien Forest2017-04-04
| | | |
| | | * Bad correction in previous commitGravatar Julien Forest2017-04-04
| | | |
| | | * Solving first problem in bug #4306. TO DO : solve the let in problemGravatar Julien Forest2017-04-04
| | | |
| * | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
| |\ \ \ | |/ / / |/| | |
| * | | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | | | | | | | | | | | | | | | | | | | | | The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step.
| * | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| |\ \ \
* | | | | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information.
* | | | | Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | | | RawLocal -> CLocal
* | | | | Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | | | This is a bit long, but it is to keep a symmetry with constr_expr.
* | | | | "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
| |/ / / |/| | |
| | * | Improving the API of constrexpr_ops.mli.Gravatar Hugo Herbelin2017-03-23
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Deprecating abstract_constr_expr in favor of mkCLambdaN, prod_constr_expr in favor of mkCProdN. Note: They did not do exactly the same, the first ones were interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones were preserving the original sharing of the type, what I think is the correct thing to do. So, there is also a "fix" of semantic here.
* | | Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."Gravatar Maxime Dénès2017-03-23
| | | | | | | | | | | | | | | This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is an 8.6 only commit.
* | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
|\ \ \ | | |/ | |/|
| * | Merge PR#495: funind: Ignore missing info for current functionGravatar Maxime Dénès2017-03-23
| |\ \
| * | | Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Gravatar Maxime Dénès2017-03-23
| | | | | | | | | | | | | | | | | | | | This way, after we merge PR#220, scripts can be fixed in a way that is compatible with the 8.6 and trunk branches.
| | * | funind: Ignore missing info for current functionGravatar Tej Chajed2017-03-22
| |/ / | | | | | | | | | | | | | | | Fixes [Coq bug #5372](https://coq.inria.fr/bugs/show_bug.cgi?id=5372) "Anomaly: Not a valid information when defining mutual fixpoints that are not mutual with Function".
* | | Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
| | | | | | | | | | | | | | | | | | | | | This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements.
| | * Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
| | |\ | |_|/ |/| |
| | * Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough.
| | * Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr.
| | * Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Funind API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Elim API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Hipattern API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Cases API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| | * Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Extend Fast_typeops to be a replacement for TypeopsGravatar Gaetan Gilbert2016-12-12
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This brings the fix in cad44fc for #2996 to the copy of Fast_typeops.check_hyps_inclusion. Fast_typeops.constant_type checks the universe constraints instead of outputting them. Since everyone who used Typeops.constant_type just discarded the constraints they've been switched to constant_type_in which should be the same in Fast_typeops and Typeops. There are some small differences in the interfaces: - Typeops.type_of_projection <-> Fast_typeops.type_of_projection_constant to avoid collision with the internally used type_of_projection (which gives the type of [Proj(p,c)]). - check_hyps_inclusion takes [('a -> constr)] and ['a] instead of [constr] for reporting errors.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * That Function is unable to create a Fixpoint equation is a user problem,Gravatar Yves Bertot2016-10-25
| | | | | | | | not an anomaly
* | CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
| | | | | | | | | | | | | | The word "increment" is more appropriate in this case than "lifting". The world "lifting", in computer science, usually denotes something else: https://en.wikipedia.org/wiki/Lambda_lifting
* | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
| | | | | | | | | | | | | | | | | | I hadn't realized that this PR uses OCaml's 4.03 inlined records feature. I will advocate again for a switch to the latest OCaml stable version, but meanwhile, let's revert. Sorry for the noise. This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
* | Merge remote-tracking branch 'github/pr/283' into trunkGravatar Maxime Dénès2016-09-22
|\ \ | | | | | | | | | Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
* | | Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
| | | | | | | | | | | | | | | | | | There was no reason to keep them separate since quite a long time. Historically, they were making Genarg depend or not on upper strata of the code, but since it was moved to lib/ this is not justified anymore.
| * | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We get rid of tuples containing booleans (typically for universe polymorphism) by replacing them with records. The previously common idom: if pi2 kind (* polymorphic *) then ... else ... becomes: if kind.polymorphic then ... else ... To make the construction and destruction of these records lightweight, the labels of boolean arguments for universe polymorphism are now usually also called "polymorphic".
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 23:49:51 +0000