aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/vernacexpr.mli
Commit message (Expand)AuthorAge
* Axioms now support the universe binding syntax.Gravatar Pierre-Marie Pédrot2015-10-08
* Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
* Goptions: new value type: optional stringGravatar Enrico Tassi2015-10-08
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Documentation by giving a name to a large type.Gravatar Pierre-Marie Pédrot2015-08-19
* Code documentation of the TACTIC/VERNAC EXTEND macros.Gravatar Pierre-Marie Pédrot2015-06-29
* Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
* Putting the From parameter of the Require command into the AST.Gravatar Pierre-Marie Pédrot2015-03-27
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* Update headers.Gravatar Maxime Dénès2015-01-12
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
* Add [Info] command.Gravatar Arnaud Spiwack2014-11-01
* Feedback message: hold extra info to help routingGravatar Enrico Tassi2014-10-31
* Emit a warning for void Arguments statement (Close 3713)Gravatar Enrico Tassi2014-10-13
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
* Add a "Hint Mode ref (+ | -)*" hint for setting a global modeGravatar Matthieu Sozeau2014-09-15
* Add syntax [id]: to apply tactic to goal named id.Gravatar Hugo Herbelin2014-09-12
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
* Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)Gravatar Enrico Tassi2014-09-09
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
* Add a [Variant] declaration which allows to write non-recursive variant types.Gravatar Arnaud Spiwack2014-09-04
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* STM: VtQuery holds the id of the state it refers toGravatar Carst Tankink2014-08-04
* Adding a new "Locate Term" command, distinct from the raw "Locate" command.Gravatar Pierre-Marie Pédrot2014-07-21
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* - Add "Show Universes" to print information about universes during a proof.Gravatar Matthieu Sozeau2014-06-16
* Fix bug #3289Gravatar Matthieu Sozeau2014-06-11
* Remove the syntax [Vernac1. Vernac2. … Vernacn. ].Gravatar Arnaud Spiwack2014-06-06
* poly: remove unused attribute to STM nodes and vernac classificaitonGravatar Enrico Tassi2014-05-15
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Adding a Print Strategy vernacular command. It allows to check theGravatar Pierre-Marie Pédrot2014-03-19
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Simpl_behaviour becomes Reductionops.ReductionBehaviourGravatar Pierre Boutillier2014-02-24
* Removing the [Require "file"] syntax.Gravatar Pierre-Marie Pédrot2014-02-02
* Proof_using: new syntax + suggestionGravatar Enrico Tassi2014-01-05
* Vernac classification: allow for commands which start proofs but must be sync...Gravatar Arnaud Spiwack2013-12-04
* STM: fix for PG and "Proof term" lines.Gravatar gareuselesinge2013-11-05
* Fixes parsing of all: followed by a typechecking/evaluation command.Gravatar aspiwack2013-11-02
* Adds a new goal selector "all:".Gravatar aspiwack2013-11-02
* STM: add "Stm Wait" to wait for the slaves to complete their jobsGravatar gareuselesinge2013-10-10
* STM: new command "Stm PrintDag" to force printing the dag to /tmpGravatar gareuselesinge2013-10-07
* STM: better handle proof modesGravatar gareuselesinge2013-09-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 18:39:47 +0000