aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_proofs.ml4
AgeCommit message (Expand)Author
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias
2018-05-23[api] Move `opacity_flag` to `Proof_global`.Emilio Jesus Gallego Arias
2018-03-08Merge PR #6909: Deprecate Focus and UnfocusMaxime Dénès
2018-03-05Deprecate Focus and Unfocus.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-01[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionVincent Laporte
2017-11-29Remove "obsolete_locality" and fix STM vernac classification.Maxime Dénès
2017-10-10[vernac] Remove "Proof using" hacks from parser.Emilio Jesus Gallego Arias
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-12Remove Show Thesis command which was never implemented.Théo Zimmermann
2017-06-12Remove non-working Show Tree and Show Node commands.Théo Zimmermann
2017-06-12Remove Show Implicit Arguments command.Théo Zimmermann
2017-06-12Remove Show Goal "uid" command.Théo Zimmermann
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-23[vernac] Remove `Save thm id.` command.Emilio Jesus Gallego Arias
2017-05-23[vernac] Remove `Save.` command.Emilio Jesus Gallego Arias
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-25[location] [ast] Switch Constrexpr AST to an extensible node type.Emilio Jesus Gallego Arias
2017-04-24[location] Use Loc.located for constr_expr.Emilio Jesus Gallego Arias
2017-04-07[camlpX] Remove camlp4 compat layer.Emilio Jesus Gallego Arias
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
2016-09-11Move Ltac-specific components from G_proofs to G_ltac.Pierre-Marie Pédrot
2016-09-08Making Vernacexpr independent from Tacexpr.Pierre-Marie Pédrot
2016-08-27Support qualified identifiers in Show Match (bug #5050).Guillaume Melquiond
2016-06-16Extend Hint Mode to handle the no-head-evar caseMatthieu Sozeau
2016-01-20Update copyright headers.Maxime Dénès
2015-11-02Adding syntax "Show id" to show goal named id (shelved or not).Hugo Herbelin
2015-10-08Proof using: let-in policy, optional auto-clear, forward closure*Enrico Tassi
2015-03-22Qed export -> Qed exportingEnrico Tassi
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-01-12Update headers.Maxime Dénès
2014-12-18Proof using: New vernacular to name sets of section variablesEnrico Tassi
2014-09-15Add a "Hint Mode ref (+ | -)*" hint for setting a global modeMatthieu Sozeau
2014-06-16- Add "Show Universes" to print information about universes during a proof.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-01-05Proof_using: new syntax + suggestionEnrico Tassi
2013-09-07Change syntax of Hint Resolve to actually accept user-given priorities.msozeau
2013-04-15More functional implementation of locality_flag and program_modegareuselesinge
2012-11-07Fix reference_or_constr grammar rule to accept @t as a constrgareuselesinge
2012-10-31Change [Hints Resolve] to still accept constrs as argumentsmsozeau
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-08-08Updating headers.herbelin
2012-05-30Restore compatibility with camlp4 (some missing open Tok)letouzey
2012-05-29simplification in deps of some g_*.ml4letouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:41:05 +0000