aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-06-06Fixes the lost evars when interpreting a change with pattern tactic.Arnaud Spiwack
2014-06-06Remove the syntax [Vernac1. Vernac2. … Vernacn. ].Arnaud Spiwack
2014-06-06Make kernel reduction code parametric over the handling of universes,Matthieu Sozeau
2014-06-06Moving the [split] tactic out of the AST.Pierre-Marie Pédrot
2014-06-05Dedicated map module for type universes. It uses hashmaps, which arePierre-Marie Pédrot
2014-06-05Removing dead code from Univ.Pierre-Marie Pédrot
2014-06-04Make standard library independent of the names generated byHugo Herbelin
2014-06-04Make standard library independent of the names generated byHugo Herbelin
2014-06-04Collecting in Namegen those conventional default names that are used in diffe...Hugo Herbelin
2014-06-04Small lemma about Relations.Hugo Herbelin
2014-06-04Remove spurious Show in script.Matthieu Sozeau
2014-06-04- Better parsing and printing of named universes: Type{ident} and foo@{(ident...Matthieu Sozeau
2014-06-04Fix canonical structure resolution (makes test-suite files go through again).Matthieu Sozeau
2014-06-04- Allow parsing of @const@{instance} for specifying universe instances of pol...Matthieu Sozeau
2014-06-04- Force every universe level to be >= Prop, so one cannot "go under" it anymore.Matthieu Sozeau
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
2014-06-04Fix handling of anonymous Type in template universe polymorphic inductivesMatthieu Sozeau
2014-06-04- Keep all <= constraints during refinement, otherwise we might miss collapse...Matthieu Sozeau
2014-06-04cbn understand ! Arguments directivePierre Boutillier
2014-06-03A bug has been closed (HoTT/coq #105)Jason Gross
2014-06-03The tactic interpreter now uses a new type of tactics, throughPierre-Marie Pédrot
2014-06-02Fixing incorrect printf format.Pierre-Marie Pédrot
2014-06-02Removing symmetry from the atomic tactics.Pierre-Marie Pédrot
2014-06-01A little bit of documentation about V5.10 and V6.3 and V7.Hugo Herbelin
2014-06-01Use of "H"-based names for propositional hypotheses obtained byHugo Herbelin
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
2014-05-31More on injection over a projectable "existT". - Fixing syntax "injection ......Hugo Herbelin
2014-05-31Fixing introduction patterns * and ** when used in a branch so that they do n...Hugo Herbelin
2014-05-31Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").Hugo Herbelin
2014-05-31Basic lemmas about the algebraic structure of equality.Hugo Herbelin
2014-05-31Dead code + typo.Hugo Herbelin
2014-05-30Adding test-suite for bug #3355.Pierre-Marie Pédrot
2014-05-28- Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed someMatthieu Sozeau
2014-05-27Removing a tclSENSITIVE from rewrite.Pierre-Marie Pédrot
2014-05-26Cbn reduces Pos.compare p~1 q~1 to Pos.compare p qPierre Boutillier
2014-05-26Reduction.Stack.Fix/Case stores Cst_stack.tPierre Boutillier
2014-05-26Cst_stack before stack (abstraction leak in whd_gen)Pierre Boutillier
2014-05-26cbn: args list instead of arg numberPierre Boutillier
2014-05-26Reductionops.Stack.map & Reduction.iterate_whd_genPierre
2014-05-26- Fix in kernel conversion not folding the universe constraintsMatthieu Sozeau
2014-05-26Update infer_conv to record trivial Prop <= Type i constraints that are neede...Matthieu Sozeau
2014-05-26make coqdep canonicalize paths from the command lineGregory Malecha
2014-05-26Fixing commit 9cef834. The parsing rules were generating an empty list,Pierre-Marie Pédrot
2014-05-24Revert "Chasing the goal entering backward while interpreting tactics. This r...Pierre-Marie Pédrot
2014-05-24Chasing the goal entering backward while interpreting tactics. This requiredPierre-Marie Pédrot
2014-05-24Fixing TACTIC EXTEND for arguments-free tactics that may modify the wholePierre-Marie Pédrot
2014-05-24Complying with reference manual for the syntax of exists/eexists, i.e.Hugo Herbelin
2014-05-22Moving the "specialize" tactic out of the AST. Also removed an obsoletePierre-Marie Pédrot
2014-05-22Fix native_compute for systems with a limited size for the command line.Guillaume Melquiond
2014-05-22Ignore generated file.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 21:21:11 +0000