| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-01-23 | Implement support for universe binder lists in Instance and Program ↵ | Matthieu Sozeau | |
| Fixpoint/Definition. | |||
| 2016-01-20 | Update copyright headers. | Maxime Dénès | |
| 2015-11-02 | Adding syntax "Show id" to show goal named id (shelved or not). | Hugo Herbelin | |
| 2015-10-08 | Axioms now support the universe binding syntax. | Pierre-Marie Pédrot | |
| We artificially restrict the syntax though, because it is unclear of what the semantics of several axioms in a row is, in particular about the resolution of remaining evars. | |||
| 2015-10-08 | Goptions: new value type: optional string | Enrico Tassi | |
| These options can be set to a string value, but also unset. Internal data is of type string option. | |||
| 2015-09-14 | Univs: Add universe binding lists to definitions | Matthieu Sozeau | |
| ... lemmas and inductives to control which universes are bound and where in universe polymorphic definitions. Names stay outside the kernel. | |||
| 2015-06-26 | Introduction of a "Undelimit Scope" command, undoing "Delimit Scope" | Lionel Rieg | |
| 2015-05-04 | Add a [Redirect] vernacular command | Clément Pit--Claudel | |
| The command [Redirect "filename" (...)] redirects all the output of [(...)] to file "filename.out". This is useful for storing the results of an [Eval compute], for redirecting the results of a large search, for automatically generating traces of interesting developments, and so on. | |||
| 2015-04-23 | Remove almost all the uses of string concatenation when building error messages. | Guillaume Melquiond | |
| Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure. | |||
| 2015-03-27 | Putting the From parameter of the Require command into the AST. | Pierre-Marie Pédrot | |
| 2015-02-14 | Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior | Enrico Tassi | |
| Of course such proofs cannot be processed asynchronously | |||
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2014-12-18 | Proof using: New vernacular to name sets of section variables | Enrico Tassi | |
| 2014-12-15 | About now accepts hypothesis names and goal selector. | Pierre Courtieu | |
| 2014-12-12 | Searchxxx now search also the hypothesis and support goal selector. | Pierre Courtieu | |
| Documentation also updated. | |||
| 2014-11-10 | Plug the dynamic tags in the Richpp mechanism. | Pierre-Marie Pédrot | |
| 2014-11-05 | lib/RichPp: Rename into Richpp. | Yann Régis-Gianas | |
| printing/RichPrinter: Rename into Richprinter. printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp. printing/Richprinter: Cosmetics. | |||
| 2014-11-05 | printing/Ppvernac: Fix missing keyword tagging on theorem introducers. | Yann Régis-Gianas | |
| 2014-11-05 | printing/Ppvernac: Fix missing keyword tagging on definition introducers. | Yann Régis-Gianas | |
| 2014-11-05 | printing/Ppvernac: Cosmetics. | Yann Régis-Gianas | |
| 2014-11-04 | printing/Ppannotation: New annotation for tactic syntactic objects. | Regis-Gianas | |
| printing/Pptactic: Tag tactics pretty-printing. printing/Ppvernac: Use the relevent Pptactic pretty-printer. printing/RichPrinter: Publish two new services. | |||
| 2014-11-04 | Rebase artefact. | Regis-Gianas | |
| 2014-11-04 | lib/Pp.tag: New. | Regis-Gianas | |
| A combinator to introduce tags. printing/{Ppconstr, Ppvernac}: Use it. | |||
| 2014-11-04 | printing/Ppannotation: Introduce a new annotation for keywords. | Regis-Gianas | |
| printing/{Ppconstr, Ppvernac}: Use it. | |||
| 2014-11-04 | Ppannotation.t: New constructor AVernac. | Regis-Gianas | |
| Ppvernac.RichPp: New rich pretty-printer. | |||
| 2014-11-04 | Ppvernac.Make: New | Regis-Gianas | |
| - Ppvernac is now functorized with respect to a Ppconstr printer. - Preserve previous behavior by instantiating this functor with Ppconstr. | |||
| 2014-11-04 | Ppvernac: Cosmetics. | Regis-Gianas | |
| 2014-11-01 | Add [Info] command. | Arnaud Spiwack | |
| Called with [Info n tac], runs [tac] and prints its info trace unfolding [n] level of tactic names ([0] for no unfolding at all). | |||
| 2014-10-13 | Emit a warning for void Arguments statement (Close 3713) | Enrico Tassi | |
| 2014-09-30 | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin | |
| will name the goal id; writing ?[?id] will use the first fresh name available based with prefix id. Tactics intro, rename, change, ... from logic.ml now preserve goal name; cut preserves goal name on its main premise. | |||
| 2014-09-29 | Notation: option to attach extra pretty printing rules to notations | Enrico Tassi | |
| so that one can retrieve them and pass them to third party tools (i.e. print the AST with the notations attached to the nodes concerned). Available syntax: - all in one: Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2"). - a posteriori: Format Notation "a /\ b" "latex" "#1 \wedge #2". | |||
| 2014-09-25 | Improve consistency of whitespace (beautifier). | Xavier Clerc | |
| 2014-09-15 | Add a "Hint Mode ref (+ | -)*" hint for setting a global mode | Matthieu Sozeau | |
| of resulution for goals whose head is "ref". + means the argument is an input and shouldn't contain an evar, otherwise resolution fails. This generalizes the Typeclasses Strict Resolution option which prevents resolution to fire on underconstrained typeclass constraints, now the criterion can be applied to specific parameters. Also cleanup auto/eauto code, uncovering a potential backwards compatibility issue: in cases the goal contains existentials, we never use the discrimination net in auto/eauto. We should try to set this on once the contribs are stabilized (the stdlib goes through when the dnet is used in these cases). | |||
| 2014-09-12 | Add syntax [id]: to apply tactic to goal named id. | Hugo Herbelin | |
| 2014-09-10 | VernacExtend does not dispatch on type anymore. | Pierre-Marie Pédrot | |
| 2014-09-04 | Remove [Infer] option of records. | Arnaud Spiwack | |
| Dead code formerly used by the now defunct [autoinstances]. | |||
| 2014-09-04 | Add a [Variant] declaration which allows to write non-recursive variant types. | Arnaud Spiwack | |
| Just like the [Record] keyword allows only non-recursive records. | |||
| 2014-08-21 | Improve consistency of whitespace (beautifier). | Xavier Clerc | |
| 2014-08-21 | Improve consistency of whitespace (beautifier). | Xavier Clerc | |
| 2014-08-21 | Space after [identity] coercion keywords (beautifier). | Xavier Clerc | |
| 2014-08-21 | Avoid redundant spaces (beautifier). | Xavier Clerc | |
| 2014-08-21 | Do not drop the locality qualifier (beautifier). | Xavier Clerc | |
| 2014-08-12 | A couple of fixes/improvements in -beautify, but backtracking on | Hugo Herbelin | |
| change of printing format of forall (need more thinking). | |||
| 2014-08-05 | Uncountably many bullets (+,-,*,++,--,**,+++,...). | Hugo Herbelin | |
| 2014-08-05 | Fixing a few beautifying bugs. | Hugo Herbelin | |
| 2014-08-05 | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi | |
| par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2). | |||
| 2014-07-21 | Adding a new "Locate Term" command, distinct from the raw "Locate" command. | Pierre-Marie Pédrot | |
| The new Term version has essentially the same behaviour as the old "Locate", while the new raw searches for all types of objects. Also code merging with the "Locate Ltac". Fixes bug #3380. | |||
| 2014-07-01 | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau | |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot | |
| 2014-06-16 | - Add "Show Universes" to print information about universes during a proof. | Matthieu Sozeau | |
| - Remove dead code in evarconv. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |