| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-19 | Remove STM vernaculars. | Maxime Dénès | |
| 2017-09-15 | Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵ | Maxime Dénès | |
| top of the linking chain. | |||
| 2017-09-15 | Merge PR #1037: Parse directly to Sorts.family when appropriate. | Maxime Dénès | |
| 2017-09-12 | Don't exclude a priori CLocalDef to be treated by ppconstr.ml. | Hugo Herbelin | |
| 2017-09-08 | Parse directly to Sorts.family when appropriate. | Gaëtan Gilbert | |
| When we used to parse to a glob_sort but always give an empty list in the GType case we can now parse directly to Sorts.family. | |||
| 2017-08-29 | [vernac] Store Infix Modifier in Vernac Notation. | Pierre-Marie Pédrot | |
| This removes a dependency from `G_vernac` to `Metasyntax`. | |||
| 2017-08-29 | Merge PR #916: Fixing notation bug 5608 involving { } and a slight ↵ | Maxime Dénès | |
| restructuration | |||
| 2017-08-29 | Merge PR #830: Moving assert (the "Cut" rule) to new proof engine | Maxime Dénès | |
| 2017-08-29 | A new step of restructuration of notations. | Hugo Herbelin | |
| This allows to issue a more appropriate message when a notation with a { } cannot be defined because of an incompatible level. E.g.: Notation "{ A } + B" := (sumbool A B) (at level 20). | |||
| 2017-08-16 | Merge PR #912: Detyping functions are now operating on EConstr.t. | Maxime Dénès | |
| 2017-08-16 | Merge PR #864: Some cleanups after cumulativity for inductive types | Maxime Dénès | |
| 2017-08-01 | Printing goals does not evar-normalizes beforehand anymore. | Pierre-Marie Pédrot | |
| 2017-08-01 | Detyping functions are now operating on EConstr.t. | Pierre-Marie Pédrot | |
| This was already the case, but the API was not exposing this. | |||
| 2017-08-01 | Merge PR #919: Remove a few useless evar-normalizations in printing code. | Maxime Dénès | |
| 2017-07-31 | Improve errors for cumulativity when monomorphic | Amin Timany | |
| We now only issue an error for locally specified (non)cumulativity whenever it is the context (set locally or globally) is monorphic. | |||
| 2017-07-31 | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | Maxime Dénès | |
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík | |
| 2017-07-26 | Remove a few useless evar-normalizations in printing code. | Pierre-Marie Pédrot | |
| 2017-07-26 | Removing template polymorphism for definitions. | Pierre-Marie Pédrot | |
| The use of template polymorphism in constants was quite limited, as it only applied to definitions that were exactly inductive types without any parameter whatsoever. Furthermore, it seems that following the introduction of polymorphic definitions, the code path enforced regular polymorphism as soon as the type of a definition was given, which was in practice almost always. Removing this feature had no observable effect neither on the test-suite, nor on any development that we monitor on Travis. I believe it is safe to assume it was nowadays useless. | |||
| 2017-07-20 | Merge PR #899: [general] Move files to directories so they match linking order. | Maxime Dénès | |
| 2017-07-19 | Merge PR #770: [proof] Move bullets to their own module. | Maxime Dénès | |
| 2017-07-19 | [general] Move files to directories matching linking order. | Emilio Jesus Gallego Arias | |
| We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`, `Miscprint`) to their proper place as they were declared in different `mllib` files than the one in their directory. In some cases this could be refined but we don't do anything fancy, we just reflect the status quo. | |||
| 2017-07-13 | Remove the function Global.type_of_global_unsafe. | Pierre-Marie Pédrot | |
| 2017-07-13 | The only abstraction-breaking function in Univ is now AUContext.instance. | Pierre-Marie Pédrot | |
| 2017-07-13 | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global. | Pierre-Marie Pédrot | |
| 2017-07-13 | Safer API for Global.body_of_constant and variants. | Pierre-Marie Pédrot | |
| We aditionally return the abstract universe context inside the option. This is relatively painless as most uses were using the option as a boolean. | |||
| 2017-07-11 | Moving the last bits of abtraction-breaking code out of the kernel. | Pierre-Marie Pédrot | |
| 2017-07-11 | Safe API for accessing universe constraints of global references. | Pierre-Marie Pédrot | |
| Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel. | |||
| 2017-07-06 | Merge PR #853: Clean 'with Definition' implementation. | Maxime Dénès | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2017-07-03 | Removing a few suspicious functions from the kernel. | Pierre-Marie Pédrot | |
| These functions were messing with the deferred universe constraints in an error-prone way, and were only used for printing as of today. We inline the one used by the printer instead. | |||
| 2017-06-25 | Moving "assert" (internally "Cut") to the new proof engine. | Hugo Herbelin | |
| It allows in particular to have "Info" on tactic "assert" and derivatives not to give an "<unknown>". | |||
| 2017-06-21 | [vernac] Remove stale bool parameter from `VernacStartTheoremProof` | Emilio Jesus Gallego Arias | |
| `VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today. | |||
| 2017-06-16 | Clean up universes of constants and inductives | Amin Timany | |
| 2017-06-16 | Add printing of cumulativity in inductive types | Amin Timany | |
| 2017-06-16 | Fix bugs and add an option for cumulativity | Amin Timany | |
| 2017-06-16 | Using UInfoInd for universes in inductive types | Amin Timany | |
| It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping. | |||
| 2017-06-15 | Merge PR#719: Constrexpr.Numeral without bigint | Maxime Dénès | |
| 2017-06-15 | Merge PR#769: [lib] Remove obsolete state-management function add_frozen_state | Maxime Dénès | |
| 2017-06-14 | Merge PR#763: [proof] Deprecate redundant wrappers. | Maxime Dénès | |
| 2017-06-14 | Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t) | Pierre Letouzey | |
| This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml | |||
| 2017-06-12 | [proof] Move bullets to their own module. | Emilio Jesus Gallego Arias | |
| Bullets were placed inside the `Proof_global` module, I guess that due to the global registration function. However, it has logically nothing to do with the functionality of `Proof_global` and the current placement may create some interference between the developers reworking proof state handling and bullets. We thus put the bullet functionality into its own, independent file. | |||
| 2017-06-12 | [lib] Remove obsolete state-management function add_frozen_state | Emilio Jesus Gallego Arias | |
| AFAICS this function predates modern state-handling; nowadays summaries are stored by the STM and nobody were using this information. | |||
| 2017-06-12 | Remove Show Thesis command which was never implemented. | Théo Zimmermann | |
| 2017-06-12 | Remove non-working Show Tree and Show Node commands. | Théo Zimmermann | |
| 2017-06-12 | Remove Show Implicit Arguments command. | Théo Zimmermann | |
| The command has been broken for 15 years. It is basically dead code. Its former behavior can be mimicked with Set Printing Implicit. Show. | |||
| 2017-06-11 | [proof] Deprecate redundant wrappers. | Emilio Jesus Gallego Arias | |
| As we would like to reduce the role of proof_global in future versions, we start to deprecate old compatibility aliases in `Pfedit` in favor of the real functions underlying the 8.5 proof engine. We also deprecate a couple of alias types and explicitly mark the few remaining uses of `Pfedit`. | |||
| 2017-06-06 | Merge PR#716: Don't double up on periods in anomalies | Maxime Dénès | |
| 2017-06-05 | Merge PR#722: [printing] Remove duplicated printing function. | Maxime Dénès | |
| 2017-06-02 | Drop '.' from CErrors.anomaly, insert it in args | Jason Gross | |
| As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ``` | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |