| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-05 | Remove dead code and unused open. | Maxime Dénès | |
| 2017-05-05 | Merge PR#558: Adding a fold_glob_constr_with_binders combinator | Maxime Dénès | |
| 2017-05-02 | Merge PR#582: Fix warnings | Maxime Dénès | |
| 2017-04-28 | Revert "Renaming allow_patvar flag of intern_gen into pattern_mode." | Maxime Dénès | |
| This reverts commit 7bdfa1a4e46acf11d199a07bfca0bc59381874c3. | |||
| 2017-04-28 | Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"." | Maxime Dénès | |
| I'm sure this was pushed by accident, since testing shows immediately that it breaks the compilation of the ssreflect plugin, hence all developments relying on it in Travis. | |||
| 2017-04-28 | Using a more explicit algebraic type for evars of kind "MatchingVar". | Hugo Herbelin | |
| A priori considered to be a good programming style. | |||
| 2017-04-28 | Renaming allow_patvar flag of intern_gen into pattern_mode. | Hugo Herbelin | |
| This highlights that this is a binary mode changing the interpretation of "?x" rather than additionally allowing patvar. | |||
| 2017-04-28 | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵ | Maxime Dénès | |
| let-ins | |||
| 2017-04-27 | Fix 4.04 warnings | Gaetan Gilbert | |
| 2017-04-27 | Warning 29: non escaped end of line may be non portable | Gaetan Gilbert | |
| 2017-04-27 | Remove unused [open] statements | Gaetan Gilbert | |
| 2017-04-27 | Remove some unused values and types | Gaetan Gilbert | |
| 2017-04-20 | correcting a typo in a comment | Matej Kosik | |
| 2017-04-15 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-04-13 | Adding a fold_glob_constr_with_binders combinator. | Hugo Herbelin | |
| Binding generalizable_vars_of_glob_constr, occur_glob_constr, free_glob_vars, and bound_glob_vars on it. Most of the functions of which it factorizes the code were bugged with respect to bindings in the return clause of "match" and in either the types or the bodies of "fix/cofix". | |||
| 2017-04-12 | Merge PR#441: Port Toplevel to the Stm API | Maxime Dénès | |
| 2017-04-12 | [flags] Documentation and a minor tweak. | Emilio Jesus Gallego Arias | |
| Mostly documentation and making a couple of local flags, local. | |||
| 2017-04-12 | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵ | Maxime Dénès | |
| record fields. | |||
| 2017-04-09 | More explicit message when a {struct x} argument refers to a local definition. | Hugo Herbelin | |
| 2017-04-05 | Fixing #5454 (an assert false with 'pat). | Hugo Herbelin | |
| Note: Apparently not easy to make a test file as the error is raised in "G_vernac.fresh_var" at parsing time (not captured by Fail). | |||
| 2017-04-04 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 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 | Using the same type of binders for interning and externing. | Hugo Herbelin | |
| Previously a union type was used for externing. In particular, moving extended_glob_local_binder to glob_constr.ml. | |||
| 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 | Merging glob_binder and glob_decl. | Hugo Herbelin | |
| 2017-03-24 | Type extended_glob_local_binder now contains only glob_constr. | Hugo Herbelin | |
| No more constr_expr in it. | |||
| 2017-03-24 | Standardized the order of constructors for binders: Assum then Def. | Hugo Herbelin | |
| 2017-03-24 | Cleaning phase around local binder at glob level: | Hugo Herbelin | |
| Aligned the type binder_data to the naming scheme used in (raw) local_binder and Rel.Declaration.t. Made some code factorization. Still to do: align type Glob_term.glob_binder to the Assum/Def format too. Note: this includes fix of anomaly with 'pat in cofix (dec77f282). | |||
| 2017-03-24 | "Standardizing" the name LocalPatten into LocalRawPattern. | Hugo Herbelin | |
| 2017-03-23 | Factorizing/unifying code in dealing with binders. | Hugo Herbelin | |
| Note: This reveals a little bug yet to fix in g_vernac.ml4. In Definition f '((x,y):id nat * id nat) '((x',y'):id nat * id nat) := Eval unfold id in x+y = x'+y'. the "id" are wrongly unfolded and in Definition f '(x,y) '(x',y') := x+y = x'+y' : Prop. an unexpected cast remains in the body of f. | |||
| 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-14 | [safe_string] interp/dumpglob | Emilio Jesus Gallego Arias | |
| No functional change. | |||
| 2017-02-22 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-02-20 | Merge PR#189: Remove tabulation support from pretty-printing. | Maxime Dénès | |
| 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 | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | |
| 2017-02-14 | Ltac now uses evar-based constrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Reductionops now return EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Tactics API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Pretyping API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Classops API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Reductionops API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-09 | Turning an anomaly on 'pat into a proper "unsupported" error message. | Hugo Herbelin | |
| 2017-02-02 | Fixing an anomaly with 'pat after cofix. | Hugo Herbelin | |
| 2017-02-01 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-01-26 | Fixing #5326 (anomaly on some unsupported case of 'pat). | Hugo Herbelin | |
| We complete the support of 'pat in this particular case (a 'pat under a binder in a notation). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |