aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.Gravatar Arnaud Spiwack2014-08-01
* Add [numgoal] to Ltac.Gravatar Arnaud Spiwack2014-08-01
* Continuing (incomplete) cleaning of Inductiveops.Gravatar Hugo Herbelin2014-08-01
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Small refactoring in Ltac parsing rules.Gravatar Arnaud Spiwack2014-07-29
* Allow [uconstr:c] as argument of a tactic.Gravatar Arnaud Spiwack2014-07-29
* Untyped terms in tactic: function [type_term c] to give a typed version of [c].Gravatar Arnaud Spiwack2014-07-29
* Untyped term in tactics: add an grammar entry to construct them.Gravatar Arnaud Spiwack2014-07-29
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
* Distinguish tactics t1;t2 and t1;[t2..].Gravatar Arnaud Spiwack2014-07-24
* Adding a new "Locate Term" command, distinct from the raw "Locate" command.Gravatar Pierre-Marie Pédrot2014-07-21
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 00:58:45 +0000