aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* The unifying functions of Rewrite uses the return types of strategies.Gravatar Pierre-Marie Pédrot2014-09-15
* Splitting the uses of the unification function according to the status ofGravatar Pierre-Marie Pédrot2014-09-15
* Rewrite.apply_strategy uses the same return type as strategies.Gravatar Pierre-Marie Pédrot2014-09-14
* Proper type for rewrite strategy results.Gravatar Pierre-Marie Pédrot2014-09-14
* Prepare goal name printing but no not print them at the current time.Gravatar Hugo Herbelin2014-09-13
* Using "Evd.restrict" in tactic clear so as to keep evar names.Gravatar Hugo Herbelin2014-09-13
* Exporting apply_subfilter from Evd.ml.Gravatar Hugo Herbelin2014-09-13
* Retroknowledge arguments are made VERNAC ARGUMENTS.Gravatar Pierre-Marie Pédrot2014-09-13
* Fixing synchronization of evar names table when merging evar_map.Gravatar Hugo Herbelin2014-09-13
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Checking typability of evar instances. Using ";" to separate bindingsGravatar Hugo Herbelin2014-09-13
* Fixing injection bug #3616 on sigma-types.Gravatar Hugo Herbelin2014-09-13
* While we don't have a clean alternative to Clenvtac, add a primitiveGravatar Matthieu Sozeau2014-09-12
* Fix base_include due to change in argument order of env and evar_mapGravatar Matthieu Sozeau2014-09-12
* An old typo which was preventing example #3537 to work the same as itGravatar Hugo Herbelin2014-09-12
* Add syntax [id]: to apply tactic to goal named id.Gravatar Hugo Herbelin2014-09-12
* Use evar name to print goal.Gravatar Hugo Herbelin2014-09-12
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* No plural for only one non existing focused goal.Gravatar Hugo Herbelin2014-09-12
* Fix source of initial goal.Gravatar Hugo Herbelin2014-09-12
* Commit 682aa67cc80 about enforcing that apply does not create newGravatar Hugo Herbelin2014-09-12
* Discontinued xml plugin: improve the README.Gravatar Arnaud Spiwack2014-09-12
* Replace the list of argument in tacexpr with a single row argument.Gravatar Arnaud Spiwack2014-09-12
* Oopps.. fixed the .ml not the .ml4Gravatar Matthieu Sozeau2014-09-11
* Use an AST for strategy names.Gravatar Matthieu Sozeau2014-09-11
* Fix test-suite files, and move some opened to closed.Gravatar Matthieu Sozeau2014-09-11
* Add a flag for restricting resolution of typeclasses toGravatar Matthieu Sozeau2014-09-11
* Keeping a sub-optimal behavior of intros_possibly_replacing for compatibility...Gravatar Hugo Herbelin2014-09-11
* Other bugs with "inversion as" (collision between user-provided names and gen...Gravatar Hugo Herbelin2014-09-11
* Fix bug #3594: eta for constructors and functions at the same time whichGravatar Matthieu Sozeau2014-09-11
* Fix bug #3596, wrong treatment of projections in compute_constelim_direct.Gravatar Matthieu Sozeau2014-09-11
* Fix bug #3505.Gravatar Matthieu Sozeau2014-09-11
* Fixing bug #3605.Gravatar Pierre-Marie Pédrot2014-09-11
* Removing remaining documentation of the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-11
* A step towards better differentiating when w_unify is used for subtermGravatar Hugo Herbelin2014-09-10
* Parsing and printing of primitive projections, fix buggy behavior whenGravatar Matthieu Sozeau2014-09-10
* Fix generation of inductive elimination principle for primitive records.Gravatar Matthieu Sozeau2014-09-10
* Fix categorization of recursive inductives.Gravatar Matthieu Sozeau2014-09-10
* Fixing localisation of tactic errors (my mistake in himsg.ml essentially).Gravatar Hugo Herbelin2014-09-10
* More small bugs in intros_replacing.Gravatar Hugo Herbelin2014-09-10
* Fixing inversion after having fixed intros_replacingGravatar Hugo Herbelin2014-09-10
* Example for apply and evars.Gravatar Hugo Herbelin2014-09-10
* Removing "eqn:" for "induction" in reference manual.Gravatar Hugo Herbelin2014-09-10
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
* - Fix printing and parsing of primitive projections, including the SetGravatar Matthieu Sozeau2014-09-09
* Merge remote-tracking branch 'jason/win32-improvements' into trunkGravatar Enrico Tassi2014-09-09
|\
| * Bump CoqSDK revision numberGravatar Jason Gross2014-09-09
| * Add a VERBOSE flag to make-sdk-win32Gravatar Jason Gross2014-09-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 06:56:24 +0000