| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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). | |||
| 2017-01-22 | Adding a new evar source to remember the name of evars which were | Hugo Herbelin | |
| named in the original term. Useful at least for debugging, useful to give a better message than "this placeholder", even if in the loc is known in this case. | |||
| 2016-10-29 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-29 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |