| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-15 | Merge PR #10150: Handle tags shorter than "diff." without an exception | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-05-15 | Merge PR #10151: Clean up the API for side-effects | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Ack-by: gares | |||
| 2019-05-14 | Merge PR #8893: Moving evars_of_term from constr to econstr | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Reviewed-by: gares Ack-by: herbelin Reviewed-by: maximedenes Reviewed-by: ppedrot | |||
| 2019-05-14 | Abstract away the implementation of side-effects in Safe_typing. | Pierre-Marie Pédrot | |
| 2019-05-14 | Allow run_tactic to return a value, remove hack from ltac2 | Gaëtan Gilbert | |
| 2019-05-13 | Handle tags shorter than "diff." without an exception | Jim Fehrle | |
| 2019-05-13 | Passing evar_map to evars_of_term rather than expecting the term to be evar-nf. | Hugo Herbelin | |
| 2019-05-13 | Moving Evd.evars_of_term from constr to econstr + consequences. | Hugo Herbelin | |
| This impacts a lot of code, apparently in the good, removing several conversions back and forth constr. | |||
| 2019-05-13 | Merge PR #10076: [Canonical structures] Annotation to field declarations to ↵ | Enrico Tassi | |
| prevent them from being “canonical” Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: robbertkrebbers Ack-by: vbgl | |||
| 2019-05-13 | Merge PR #9887: [api] Remove 8.10 deprecations. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-05-13 | Merge PR #10061: Print custom grammar entries | Vincent Laporte | |
| Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: jashug | |||
| 2019-05-10 | Use Print Custom Grammar to inspect custom entries | Jasper Hugunin | |
| 2019-05-10 | [Attributes] Allow explicit value for two-valued attributes | Vincent Laporte | |
| Attributes that enable/disable a feature can have an explicit value (default is enable when the attribute is present). Three-valued boolean attributes do not support this: what would `#[local(false)]` mean? | |||
| 2019-05-10 | [Canonical structures] “not_canonical” annotation to field declarations | Vincent Laporte | |
| 2019-05-10 | [Canonical structures] Some projections may not be canonical | Vincent Laporte | |
| 2019-05-10 | Remove various circumvolutions from reduction behaviors | Maxime Dénès | |
| Incidentally, this fixes #10056 | |||
| 2019-05-10 | [api] Remove 8.10 deprecations. | Emilio Jesus Gallego Arias | |
| Some of them are significant so presumably it will take a bit of effort to fix overlays. I left out the removal of `nf_enter` for now as MTac2 needs some serious porting in order to avoid it. | |||
| 2019-05-07 | Show diffs in error messages only if Diffs is enabled | Jim Fehrle | |
| 2019-05-07 | [Record] Une a record to gather field declaration attributes | Vincent Laporte | |
| 2019-05-07 | [Record] Deforestation | Vincent Laporte | |
| 2019-05-04 | Merge PR #9926: [vernac] [ast] Make location info an attribute of vernaculars. | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot | |||
| 2019-05-01 | [comDefinition] Use prepare function from DeclareDef. | Emilio Jesus Gallego Arias | |
| We also update the plugin tutorial. This was already tried [in the same exact way] in #8811, however the bench time was not convincing then, but now things seem a bit better, likely due to the removal of some extra normalization somewhere. Some more changes from #8811 are still pending. | |||
| 2019-04-30 | Remove Global.env from goptions by passing from vernacentries | Gaëtan Gilbert | |
| Currently this env is only used to error for Printing If/Let on non-2-constructor/non-1-constructor types so we could alternatively remove it and not error / error later when trying to print. Keeping the env and the error as-is should be fine though. | |||
| 2019-04-30 | Merge PR #10019: Update behavior of -emacs to support showing diffs in ↵ | Emilio Jesus Gallego Arias | |
| ProofGeneral (master branch) Reviewed-by: ejgallego | |||
| 2019-04-29 | Merge PR #9935: [api] [proof] Alert users that `Vernacstate.Proof_global` is ↵ | Maxime Dénès | |
| not to be used. Ack-by: ejgallego Ack-by: gares Reviewed-by: maximedenes | |||
| 2019-04-28 | Update behavior of -emacs to support showing diffs in ProofGeneral (master ↵ | Jim Fehrle | |
| branch) Adds XML-like tags in output to mark diffs | |||
| 2019-04-25 | [vernac] [ast] Make location info an attribute of vernaculars. | Emilio Jesus Gallego Arias | |
| This has been a mess for quite a while, we try to improve it. | |||
| 2019-04-17 | Merge PR #9876: Command-line setters for options | Emilio Jesus Gallego Arias | |
| Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares | |||
| 2019-04-16 | [ast] [constrexpr] Make recursion_order_expr an AST node. | Emilio Jesus Gallego Arias | |
| This is a bit more uniform. | |||
| 2019-04-16 | Clean the representation of recursive annotation in Constrexpr | Maxime Dénès | |
| We make clearer which arguments are optional and which are mandatory. Some of these representations are tricky because of small differences between Program and Function, which share the same infrastructure. As a side-effect of this cleanup, Program Fixpoint can now be used with e.g. {measure (m + n) R}. Previously, parentheses were required around R. | |||
| 2019-04-12 | Unify Set and Unset handling for options | Gaëtan Gilbert | |
| Not sure if the idetop.set_options was correctly changed, ocaml types pass at least. | |||
| 2019-04-11 | Merge PR #9909: Remove all but one call to `Global` in the pretyper | Pierre-Marie Pédrot | |
| Ack-by: ejgallego Reviewed-by: gares Ack-by: maximedenes Ack-by: ppedrot | |||
| 2019-04-10 | Merge PR #9910: [api] [proofs] Remove dependency of proofs on interp. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-04-10 | Remove calls to global env in Inductiveops | Maxime Dénès | |
| 2019-04-10 | Remove calls to Global.env and Libobject from Recordops | Maxime Dénès | |
| 2019-04-10 | Functionalize env in type classes | Maxime Dénès | |
| I had to reorganize the code a bit. The Context command moved to comAssumption, as it is not so related to type classes. We were able to remove a few hooks on the way. | |||
| 2019-04-10 | Move vernac-related part of coercions to vernac | Maxime Dénès | |
| 2019-04-10 | Improve SProp error message to mention the Allow StrictProp flag. | Théo Zimmermann | |
| And document the error message. | |||
| 2019-04-09 | [api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used. | Emilio Jesus Gallego Arias | |
| We alert users that `Vernacstate.Proof_global` is a Coq internal module and should not be used to workaround lack of state threading. | |||
| 2019-04-05 | [api] [proofs] Remove dependency of proofs on interp. | Emilio Jesus Gallego Arias | |
| We perform some cleanup and remove dependency of `proofs/` on `interp/`, which seems logical. In fact, `interp` + `parsing` are quite self-contained, so if there is interest we could also make tactics to depend directly on proofs. | |||
| 2019-04-05 | Merge PR #9685: [vernac] Small cleanup to remove assert false. | Vincent Laporte | |
| Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: vbgl | |||
| 2019-04-05 | Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01) | Emilio Jesus Gallego Arias | |
| Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: herbelin Ack-by: ppedrot Ack-by: proux01 | |||
| 2019-04-03 | Merge PR #9861: [program] Allow evars in type of fixpoints. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-04-03 | Merge PR #8638: Remove -compat 8.7 | Théo Zimmermann | |
| Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: jfehrle Ack-by: maximedenes Reviewed-by: ppedrot | |||
| 2019-04-02 | Merge PR #8984: Declare initial hint databases in prelude | Pierre-Marie Pédrot | |
| Ack-by: JasonGross Reviewed-by: ppedrot | |||
| 2019-04-02 | Remove -compat 8.7 | Jason Gross | |
| This removes various compatibility notations. Closes #8374 This commit was mostly created by running `./dev/tools/update-compat.py --release`. There's a bit of manual spacing adjustment around all of the removed compatibility notations, and some test-suite updates were done manually. The update to CHANGES.md was manual. | |||
| 2019-04-02 | Add parsing of decimal constants (e.g., 1.02e+01) | Pierre Roux | |
| Rather than integers '[0-9]+', numeral constant can now be parsed according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'. This can be used in one of the two following ways: - using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin - using `Numeral Notation` with the type `decimal` added to `Decimal.v` See examples of each use case in the next two commits. | |||
| 2019-04-02 | Rename raw_natural_number to raw_numeral | Pierre Roux | |
| In anticipation of an extension from natural numbers to other numeral constants. | |||
| 2019-04-02 | Rename the INT token to NUMERAL | Pierre Roux | |
| In anticipation of future uses of this token for non integer numerals. | |||
| 2019-04-01 | Replace type sign = bool with SPlus | SMinus | Pierre Roux | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |