aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_proofs.ml4
Commit message (Expand)AuthorAge
* 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
* Removing PrintConstr debugging entry in g_proof.ml4 which was notGravatar herbelin2011-12-18
* Proof using ...Gravatar gareuselesinge2011-12-12
* Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...Gravatar aspiwack2011-09-12
* - Fix treatment of globality flag for typeclass instance hints (theyGravatar msozeau2011-02-14
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Remove Explain* vernacsGravatar glondu2010-10-06
* Remove VernacGoGravatar glondu2010-10-06
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* static (and shared) camlp4use instead of per-file declarationGravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* Fixing/improving management of uniform prefix Local and GlobalGravatar herbelin2009-01-14
* - Standardized prefix use of "Local"/"Global" modifiers as decided inGravatar herbelin2009-01-13