aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_proofs.ml4
Commit message (Expand)AuthorAge
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionGravatar Vincent Laporte2018-02-01
* Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
* [vernac] Remove "Proof using" hacks from parser.Gravatar Emilio Jesus Gallego Arias2017-10-10
* [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove Show Thesis command which was never implemented.Gravatar Théo Zimmermann2017-06-12
* Remove non-working Show Tree and Show Node commands.Gravatar Théo Zimmermann2017-06-12
* Remove Show Implicit Arguments command.Gravatar Théo Zimmermann2017-06-12
* Remove Show Goal "uid" command.Gravatar Théo Zimmermann2017-06-12
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| * [vernac] Remove `Save.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
|/
* [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\
| * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
* | Move Ltac-specific components from G_proofs to G_ltac.Gravatar Pierre-Marie Pédrot2016-09-11
* | Making Vernacexpr independent from Tacexpr.Gravatar Pierre-Marie Pédrot2016-09-08
|/
* Support qualified identifiers in Show Match (bug #5050).Gravatar Guillaume Melquiond2016-08-27
* Extend Hint Mode to handle the no-head-evar caseGravatar Matthieu Sozeau2016-06-16
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
* Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
* Qed export -> Qed exportingGravatar Enrico Tassi2015-03-22
* 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
* Add a "Hint Mode ref (+ | -)*" hint for setting a global modeGravatar Matthieu Sozeau2014-09-15
* - Add "Show Universes" to print information about universes during a proof.Gravatar Matthieu Sozeau2014-06-16
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Proof_using: new syntax + suggestionGravatar Enrico Tassi2014-01-05
* Change syntax of Hint Resolve to actually accept user-given priorities.Gravatar msozeau2013-09-07
* More functional implementation of locality_flag and program_modeGravatar gareuselesinge2013-04-15
* Fix reference_or_constr grammar rule to accept @t as a constrGravatar gareuselesinge2012-11-07
* Change [Hints Resolve] to still accept constrs as argumentsGravatar msozeau2012-10-31
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
* Updating headers.Gravatar herbelin2012-08-08
* Restore compatibility with camlp4 (some missing open Tok)Gravatar letouzey2012-05-30
* simplification in deps of some g_*.ml4Gravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Vernacexpr is now a mli-only file, locality stuff now in locality.mlGravatar letouzey2012-05-29
* Removed syntax BeginSubproof/EndSubproof. It has been replaced byGravatar aspiwack2012-04-13
* Added a command "Unfocused" which returns an error when the proof isGravatar aspiwack2012-03-30
* Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconclGravatar letouzey2012-03-30
* Remove old proof-managment commands Suspend/ResumeGravatar letouzey2012-03-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 19:21:39 +0000