aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Removing the [Require "file"] syntax.Gravatar Pierre-Marie Pédrot2014-02-02
* G_xml: remove some duplication in error fonctionsGravatar Pierre Letouzey2014-01-30
* G_xml: protect against some possible Not_foundGravatar Pierre Letouzey2014-01-30
* Documenting old but useful command "Print Tables".Gravatar Hugo Herbelin2014-01-13
* Fixing bug #3144.Gravatar Pierre-Marie Pédrot2014-01-10
* Proof_using: new syntax + suggestionGravatar Enrico Tassi2014-01-05
* Removing the useless pattern ident genarg.Gravatar Pierre-Marie Pédrot2013-12-19
* Patch for supporting [From Xxx Require Yyy Zzz.]Gravatar Gregory Malecha2013-12-12
* Vernac classification: allow for commands which start proofs but must be sync...Gravatar Arnaud Spiwack2013-12-04
* Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30
* Actually adding the grammar entry to handle tactics in terms.Gravatar Pierre-Marie Pédrot2013-11-27
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-10
* Revert the previous commit. It broke Coq compilation.Gravatar ppedrot2013-11-09
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-09
* Moving notation types into grammar rule.Gravatar ppedrot2013-11-09
* Cleaning and documenting Egramcoq.Gravatar ppedrot2013-11-09
* empty token in terminal is a user error not an anomaly (bug 3118)Gravatar pboutill2013-11-03
* Adds an experimental exactly_once tactical.Gravatar aspiwack2013-11-02
* Adds a tactical once.Gravatar aspiwack2013-11-02
* Added the tactical "tac1 + tac2".Gravatar aspiwack2013-11-02
* Fixes parsing of all: followed by a typechecking/evaluation command.Gravatar aspiwack2013-11-02
* New option Default Goal Selector.Gravatar aspiwack2013-11-02
* Adds a new goal selector "all:".Gravatar aspiwack2013-11-02
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
* Removing some generic equalities.Gravatar ppedrot2013-10-22
* STM: add "Stm Wait" to wait for the slaves to complete their jobsGravatar gareuselesinge2013-10-10
* STM: new command "Stm PrintDag" to force printing the dag to /tmpGravatar gareuselesinge2013-10-07
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Change syntax of Hint Resolve to actually accept user-given priorities.Gravatar msozeau2013-09-07
* * parsing/Lexer: Cosmetics.Gravatar regisgia2013-09-02
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Modulification and removing of structural equality in Stateid.Gravatar ppedrot2013-08-19
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
* Support Proof GeneralGravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Added a Print Debug GC command that displays the current state ofGravatar ppedrot2013-08-01
* Granting bug #3098: adding priority to Existing Instances.Gravatar ppedrot2013-08-01
* More dynamic argument scopesGravatar letouzey2013-07-17
* Added a Register Inline command for the native compiler. Will be ported to th...Gravatar mdenes2013-07-10
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
* Reorganizing intropatterns: * and ** are not naming intropatterns.Gravatar herbelin2013-07-09
* Expurgating the useless difference between List0 and List1 at theGravatar ppedrot2013-07-05
* Removing the use of leveled tactics wit_tacticn. It is now handledGravatar ppedrot2013-07-02
* Removed the ad-hod handling of wit_tacticn.Gravatar ppedrot2013-07-02
* Fixing Camlp4 compilation.Gravatar ppedrot2013-06-30