| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-04-07 | Fixing #4499 (not using unnamed record field in {| |} notation). | 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 | |
| 2016-10-27 | Fixing #5161 (case of a notation with unability to detect a recursive binder). | Hugo Herbelin | |
| Type annotations in unrelated binders were badly interfering with detection of recursive binders in notations. | |||
| 2016-10-19 | CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript". | Matej Kosik | |
| 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 | |||
| 2016-10-17 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-17 | Merge PR #310 into v8.5 | Pierre-Marie Pédrot | |
| 2016-10-17 | Merge PR #310 into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-12 | Merge PR #289 into v8.6. | Pierre-Marie Pédrot | |
| 2016-10-12 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-12 | Fixing a collision about the meta-variable ".." in recursive notations. | Hugo Herbelin | |
| This happens when recursive notations are used to define recursive notations. | |||
| 2016-10-12 | Shorter message for "Test Asymmetric Patterns". | Hugo Herbelin | |
| But maybe it is that how the "Test" message is elaborated is not intuitive... | |||
| 2016-10-12 | Fixing a few confusions on the name of the beautify flag. | Hugo Herbelin | |
| (It should apply also interactively.) | |||
| 2016-10-08 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-06 | Revert "Make the pretty printer resilient to incomplete nametab (progress on ↵ | Théo Zimmermann | |
| #4363)." This reverts commit 11ccb7333c2a82d59736027838acaea2237e2402. This fixes bug #4874. We fallback to the original error message of v8.4. The fallback printer introduced in this commit only gave unqualified names, which is what this bug reports. | |||
| 2016-10-06 | Disable compatibility notations warnings. | Maxime Dénès | |
| Enablnig them would give a system that tells the user to replace e.g.: le_n_Sn with Nat.le_succ_diag_r lt_S with Nat.lt_lt_succ_r (on other types like R and and positive, the same lemma is called lt_lt_succ) In many cases, the new names will be too painful for intensive users. | |||
| 2016-10-06 | Remove the Set Verbose Compat option and turn the warning on by default. | Maxime Dénès | |
| These warnings can now be configured like any other, so we don't need a specific option anymore. | |||
| 2016-10-05 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |