aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
* time tacGravatar Hugo Herbelin2014-07-07
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Fixing #3390 (mismatch simple_tactic/tactic0 leading to segfault).Gravatar Hugo Herbelin2014-06-21
* - Add "Show Universes" to print information about universes during a proof.Gravatar Matthieu Sozeau2014-06-16
* Fix bug #3289Gravatar Matthieu Sozeau2014-06-11
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Remove the syntax [Vernac1. Vernac2. … Vernacn. ].Gravatar Arnaud Spiwack2014-06-06
* Moving the [split] tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-06-06
* - Better parsing and printing of named universes: Type{ident} and foo@{(ident...Gravatar Matthieu Sozeau2014-06-04
* - Allow parsing of @const@{instance} for specifying universe instances of pol...Gravatar Matthieu Sozeau2014-06-04
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* Removing symmetry from the atomic tactics.Gravatar Pierre-Marie Pédrot2014-06-02
* Fixing commit 9cef834. The parsing rules were generating an empty list,Gravatar Pierre-Marie Pédrot2014-05-26
* Complying with reference manual for the syntax of exists/eexists, i.e.Gravatar Hugo Herbelin2014-05-24
* Moving the "specialize" tactic out of the AST. Also removed an obsoleteGravatar Pierre-Marie Pédrot2014-05-22
* Removing useless use of metaids in tactic AST.Gravatar Pierre-Marie Pédrot2014-05-22
* Removing decompose record / sum from the tactic AST.Gravatar Pierre-Marie Pédrot2014-05-21
* Moving left & right tactics out of the AST.Gravatar Pierre-Marie Pédrot2014-05-21
* Moving (e)transitivity out of the AST.Gravatar Pierre-Marie Pédrot2014-05-20
* Tentative to add constr-using primitive tactics without grammar rules.Gravatar Pierre-Marie Pédrot2014-05-20
* Adding way to get the list of the accepted tactic notation arguments.Gravatar Pierre-Marie Pédrot2014-05-17
* Moving argument-free tactics out of the AST into a dedicatedGravatar Pierre-Marie Pédrot2014-05-16
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* Moving the ML tactic extension mechanism to a Libobject-based one.Gravatar Pierre-Marie Pédrot2014-05-12
* Cleanup before merge with the trunkGravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Closing bug #3260Gravatar Julien Forest2014-04-14
* Adding a Print Strategy vernacular command. It allows to check theGravatar Pierre-Marie Pédrot2014-03-19
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Migrate back g_obligations in toplevelGravatar Pierre Letouzey2014-03-02
* Simpl_behaviour becomes Reductionops.ReductionBehaviourGravatar Pierre Boutillier2014-02-24
* Removing non-marshallable data from the Agram constructor. Instead ofGravatar Pierre-Marie Pédrot2014-02-16
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 18:06:24 +0000