aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
* Preserve compatibility on examples such as "intros []." on goals suchGravatar Hugo Herbelin2014-06-06
* Dead code.Gravatar Hugo Herbelin2014-06-06
* Fixes the lost evars when interpreting a change with pattern tactic.Gravatar Arnaud Spiwack2014-06-06
* Remove the syntax [Vernac1. Vernac2. … Vernacn. ].Gravatar Arnaud Spiwack2014-06-06
* Make kernel reduction code parametric over the handling of universes,Gravatar Matthieu Sozeau2014-06-06
* Moving the [split] tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-06-06
* Dedicated map module for type universes. It uses hashmaps, which areGravatar Pierre-Marie Pédrot2014-06-05
* Removing dead code from Univ.Gravatar Pierre-Marie Pédrot2014-06-05
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* Small lemma about Relations.Gravatar Hugo Herbelin2014-06-04
* Remove spurious Show in script.Gravatar Matthieu Sozeau2014-06-04
* - Better parsing and printing of named universes: Type{ident} and foo@{(ident...Gravatar Matthieu Sozeau2014-06-04
* Fix canonical structure resolution (makes test-suite files go through again).Gravatar Matthieu Sozeau2014-06-04
* - Allow parsing of @const@{instance} for specifying universe instances of pol...Gravatar Matthieu Sozeau2014-06-04
* - Force every universe level to be >= Prop, so one cannot "go under" it anymore.Gravatar Matthieu Sozeau2014-06-04
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* Fix handling of anonymous Type in template universe polymorphic inductivesGravatar Matthieu Sozeau2014-06-04
* - Keep all <= constraints during refinement, otherwise we might miss collapse...Gravatar Matthieu Sozeau2014-06-04
* cbn understand ! Arguments directiveGravatar Pierre Boutillier2014-06-04
* A bug has been closed (HoTT/coq #105)Gravatar Jason Gross2014-06-03
* The tactic interpreter now uses a new type of tactics, throughGravatar Pierre-Marie Pédrot2014-06-03
* Fixing incorrect printf format.Gravatar Pierre-Marie Pédrot2014-06-02
* Removing symmetry from the atomic tactics.Gravatar Pierre-Marie Pédrot2014-06-02
* A little bit of documentation about V5.10 and V6.3 and V7.Gravatar Hugo Herbelin2014-06-01
* Use of "H"-based names for propositional hypotheses obtained byGravatar Hugo Herbelin2014-06-01
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* More on injection over a projectable "existT". - Fixing syntax "injection ......Gravatar Hugo Herbelin2014-05-31
* Fixing introduction patterns * and ** when used in a branch so that they do n...Gravatar Hugo Herbelin2014-05-31
* Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").Gravatar Hugo Herbelin2014-05-31
* Basic lemmas about the algebraic structure of equality.Gravatar Hugo Herbelin2014-05-31
* Dead code + typo.Gravatar Hugo Herbelin2014-05-31
* Adding test-suite for bug #3355.Gravatar Pierre-Marie Pédrot2014-05-30
* - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed someGravatar Matthieu Sozeau2014-05-28
* Removing a tclSENSITIVE from rewrite.Gravatar Pierre-Marie Pédrot2014-05-27
* Cbn reduces Pos.compare p~1 q~1 to Pos.compare p qGravatar Pierre Boutillier2014-05-26
* Reduction.Stack.Fix/Case stores Cst_stack.tGravatar Pierre Boutillier2014-05-26
* Cst_stack before stack (abstraction leak in whd_gen)Gravatar Pierre Boutillier2014-05-26
* cbn: args list instead of arg numberGravatar Pierre Boutillier2014-05-26
* Reductionops.Stack.map & Reduction.iterate_whd_genGravatar Pierre2014-05-26
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* Update infer_conv to record trivial Prop <= Type i constraints that are neede...Gravatar Matthieu Sozeau2014-05-26
* make coqdep canonicalize paths from the command lineGravatar Gregory Malecha2014-05-26
* Fixing commit 9cef834. The parsing rules were generating an empty list,Gravatar Pierre-Marie Pédrot2014-05-26
* Revert "Chasing the goal entering backward while interpreting tactics. This r...Gravatar Pierre-Marie Pédrot2014-05-24
* Chasing the goal entering backward while interpreting tactics. This requiredGravatar Pierre-Marie Pédrot2014-05-24
* Fixing TACTIC EXTEND for arguments-free tactics that may modify the wholeGravatar Pierre-Marie Pédrot2014-05-24
* Complying with reference manual for the syntax of exists/eexists, i.e.Gravatar Hugo Herbelin2014-05-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 02:33:09 +0000