| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-04-27 | Fix 4.04 warnings | Gaetan Gilbert | |
| 2017-04-27 | Remove unused [open] statements | Gaetan Gilbert | |
| 2017-04-27 | Remove some unused values and types | Gaetan Gilbert | |
| 2017-04-24 | Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag. | Maxime Dénès | |
| 2017-04-22 | Merge branch v8.6 into trunk | Hugo Herbelin | |
| Note: I removed what seemed to be dead code in recdef.ml (local_assum and local_def introduced with econstr branch), assuming that this is what should be done. | |||
| 2017-04-21 | [flags] Deprecate is_silent/is_verbose in favor of single flag. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-04-12 | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵ | Maxime Dénès | |
| record fields. | |||
| 2017-04-11 | Merge PR#379: Introducing evar-insensitive constrs | Maxime Dénès | |
| 2017-04-07 | [camlpX] Remove camlp4 compat layer. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-04-04 | end of correction of bug 4306 | Julien Forest | |
| 2017-04-04 | Bad correction in previous commit | Julien Forest | |
| 2017-04-04 | Solving first problem in bug #4306. TO DO : solve the let in problem | Julien Forest | |
| 2017-04-04 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-04-01 | Using delayed universe instances in EConstr. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-03-24 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-03-24 | Replacing "cast surgery" in LetIn by a proper field (see PR #404). | Hugo Herbelin | |
| 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. | |||
| 2017-03-24 | Unifying standard "constr_level" names for constructors of local_binder_expr. | Hugo Herbelin | |
| RawLocal -> CLocal | |||
| 2017-03-24 | Renaming local_binder into local_binder_expr. | Hugo Herbelin | |
| This is a bit long, but it is to keep a symmetry with constr_expr. | |||
| 2017-03-24 | "Standardizing" the name LocalPatten into LocalRawPattern. | Hugo Herbelin | |
| 2017-03-23 | Improving the API of constrexpr_ops.mli. | Hugo Herbelin | |
| 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. | |||
| 2017-03-23 | Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220." | Maxime Dénès | |
| This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is an 8.6 only commit. | |||
| 2017-03-23 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-03-23 | Merge PR#495: funind: Ignore missing info for current function | Maxime Dénès | |
| 2017-03-23 | Add empty Extraction.v and FunInd.v to prepare landing of PR#220. | Maxime Dénès | |
| This way, after we merge PR#220, scripts can be fixed in a way that is compatible with the 8.6 and trunk branches. | |||
| 2017-03-22 | funind: Ignore missing info for current function | Tej Chajed | |
| 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". | |||
| 2017-02-17 | Moving the Ltac plugin to a pack-based one. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-02-14 | Merge branch 'master'. | Pierre-Marie Pédrot | |
| 2017-02-14 | Namegen primitives now apply on evar constrs. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-02-14 | Definining EConstr-based contexts. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-02-14 | Evar-normalizing functions now act on EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | |
| 2017-02-14 | Funind API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Ltac now uses evar-based constrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Removing compatibility layers in Retyping | Pierre-Marie Pédrot | |
| 2017-02-14 | Removing some return type compatibility layers in Termops. | Pierre-Marie Pédrot | |
| 2017-02-14 | Reductionops now return EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Equality API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Elim API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Tactics API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Hipattern API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Tacmach API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Cases API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Tacred API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Typing API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Evarconv API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Reductionops API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Termops API using EConstr. | Pierre-Marie Pédrot | |
| 2016-12-12 | Extend Fast_typeops to be a replacement for Typeops | Gaetan Gilbert | |
| 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. | |||
| 2016-10-29 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-25 | That Function is unable to create a Fixpoint equation is a user problem, | Yves Bertot | |
| not an anomaly | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |