aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* While resolving typeclass evars in clenv, touch only the ones that appear in theGravatar Matthieu Sozeau2014-09-17
* Update test-suite files after last commit. Add a file for rewrite_stratGravatar Matthieu Sozeau2014-09-17
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Undo prints only if coqtop || emacsGravatar Enrico Tassi2014-09-16
* better error messageGravatar Enrico Tassi2014-09-16
* fix test-suite/success/decl_mode.vGravatar Enrico Tassi2014-09-16
* More on printing references applied to implicit arguments.Gravatar Hugo Herbelin2014-09-16
* Add a "Hint Mode ref (+ | -)*" hint for setting a global modeGravatar Matthieu Sozeau2014-09-15
* Adapting ltac output test to new interpretation of binders.Gravatar Hugo Herbelin2014-09-15
* Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.Gravatar Hugo Herbelin2014-09-15
* Not printing goal name (reinstalled by mistake in a previous commit).Gravatar Hugo Herbelin2014-09-15
* Fixing line break in test for #3559.Gravatar Hugo Herbelin2014-09-15
* Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].Gravatar Arnaud Spiwack2014-09-15
* Ltac names in binders: some Ltac values can be seen both as terms and identif...Gravatar Arnaud Spiwack2014-09-15
* Fix: when interpreting a identifier in pretying, use the Ltac identifier subs...Gravatar Arnaud Spiwack2014-09-15
* Fix a bug in the naming of binders.Gravatar Arnaud Spiwack2014-09-15
* A small pass of code cleaning and clenv removing in Rewrite.Gravatar Pierre-Marie Pédrot2014-09-15
* Fixing bug #3619 in emacs mode.Gravatar Hugo Herbelin2014-09-15
* Avoid backtracking in typeclass search if a solution for a closedGravatar Matthieu Sozeau2014-09-15
* Fix bug #3610, allowing betaiotadelta reduction while unifying types ofGravatar Matthieu Sozeau2014-09-15
* Fix bug #3621, using fold_left2 on arrays of the same size only.Gravatar Matthieu Sozeau2014-09-15
* Rework typeclass resolution and control of backtracking.Gravatar Matthieu Sozeau2014-09-15
* Removing one Evd.merge in Rewrite.Gravatar Pierre-Marie Pédrot2014-09-15
* More invariants in Rewrite unification.Gravatar Pierre-Marie Pédrot2014-09-15
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 17:38:00 +0000