| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2016-10-04 | Fix #5048 - Casts in pattern raise an anomaly in Constrintern. | Maxime Dénès | |
| We protect the code against the presence of pattern casts where they are not supported. Why we cannot make the pattern type reflect this is a long story (described in this commit), but in the long term we probably want to support them anywhere, like OCaml does. Of course, it will require to adjust the pattern matching compiler. | |||
| 2016-10-04 | Quick fix to #4595 (making notations containing "ltac:" unused for printing). | Hugo Herbelin | |
| Also getting rid of a global side-effect. | |||
| 2016-10-02 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-02 | Fix bug #5087: Improve the error message on record with duplicated fields. | Pierre-Marie Pédrot | |
| 2016-09-28 | Warning about similar notations now up to alpha-conversion. | Hugo Herbelin | |
| This allows to define on purpose the very same notation in different files, as currently the notations for *, +, - in Nat.v and Peano.v (with the first one using variables n and m and the second one using the default variables used by Infix, namely x and y). This makes also the "notation-overridden" warning less enigmatic facing two notations which are the same up to the choice of names. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |