aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_proofs.ml4
Commit message (Expand)AuthorAge
* 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
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
* Idtac peut prendre un argument à afficherGravatar narboux2003-11-12
* reorganisation des niveaux (ex: = est a 70)Gravatar barras2003-10-22
* Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...Gravatar herbelin2003-10-08
* Debranchement de l'affichage automatique de Proof par le traducteur (trop com...Gravatar herbelin2003-10-07
* Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...Gravatar herbelin2003-09-12