aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_proofs.ml4
Commit message (Expand)AuthorAge
* 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
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
* Add the ability to declare [Hint Extern]'s with no pattern.Gravatar msozeau2008-09-07
* Fixes in typeclasses resolution. Avoid reducing instances types beforeGravatar msozeau2008-09-07
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Generalized CAMLP4USE for pp dependenciesGravatar corbinea2007-07-16
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
* Suppression code pour hints nommés à la V7 (voire à la V6...)Gravatar herbelin2006-01-28
* Messages de idtac et fail peuvent maintenant être des listes de string, int ...Gravatar herbelin2006-01-21
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Nouvelle en-têteGravatar herbelin2004-07-16