aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Fixing a bug in the presence of let-in in inductive arity.Gravatar Hugo Herbelin2014-10-20
* Revert "Fixing a loop in proof reconstruction for congruence (#2447)."Gravatar Hugo Herbelin2014-10-17
* Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...Gravatar Hugo Herbelin2014-10-17
* Now printing "now a keyword" only in verbose mode.Gravatar Hugo Herbelin2014-10-17
* When facing problem ?id = ?id' in resolution of return predicate,Gravatar Hugo Herbelin2014-10-17
* Experimental printing of the signature of open evars in Check.Gravatar Hugo Herbelin2014-10-17
* New experimental heuristic printing strategy for evar instances: WeGravatar Hugo Herbelin2014-10-17
* Re-displaying evar instances in debugger.Gravatar Hugo Herbelin2014-10-17
* Fixing a loop in proof reconstruction for congruence (#2447).Gravatar Hugo Herbelin2014-10-17
* Essai où assert_style n'est utilisé que si pas visuellement une équation;Gravatar Hugo Herbelin2014-10-17
* More fallout from elisp renameGravatar Anders Kaseorg2014-10-16
* Relaxing again the test on types of replacements in tactic changeGravatar Hugo Herbelin2014-10-16
* In convert_concl/convert_hyp: nf_enter -> enter.Gravatar Hugo Herbelin2014-10-16
* Revert "Naming main goal "Main""Gravatar Hugo Herbelin2014-10-16
* Refactoring proofview: make the definition of the logic monad polymorphic.Gravatar Arnaud Spiwack2014-10-16
* Refresh to avoid algebraic universes on the right.Gravatar Matthieu Sozeau2014-10-16
* Fix test-suite scripts.Gravatar Matthieu Sozeau2014-10-16
* Bug fixed by Hugo.Gravatar Matthieu Sozeau2014-10-16
* Grab Existential Variables: restore the goal order from v8.4.Gravatar Arnaud Spiwack2014-10-16
* Proofview: cleanup: no more reference to Goal.goal.Gravatar Arnaud Spiwack2014-10-16
* Put evars remaining after a tactic on the shelf.Gravatar Arnaud Spiwack2014-10-16
* Refine: proper scoping of the future goals.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove [advance] from the API.Gravatar Arnaud Spiwack2014-10-16
* Proofview: remove unused [refresh_sigma] compatibility primitive.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove some functions from the compatibility layer.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove most of the API (make [Goal.goal] concrete).Gravatar Arnaud Spiwack2014-10-16
* Make [Goal.goal] be exactly [Evar.t].Gravatar Arnaud Spiwack2014-10-16
* Goal: remove dead code.Gravatar Arnaud Spiwack2014-10-16
* Expose Proofview.Refine.with_type in the API.Gravatar Arnaud Spiwack2014-10-16
* Proofview.Refine: remove the handle type, and simplify the API.Gravatar Arnaud Spiwack2014-10-16
* Move the handling of the principal evar from refine to evd.Gravatar Arnaud Spiwack2014-10-16
* Move the handling a new evars from the [Proofview.Refine] module to [Evd].Gravatar Arnaud Spiwack2014-10-16
* Evd: a few comments to document the increasingly wide internal [evar_map] type.Gravatar Arnaud Spiwack2014-10-16
* Evd: remove/update obsolete comments.Gravatar Arnaud Spiwack2014-10-16
* Proofview.Refine: delay the marking of new evars as goals from [new_evar] to ...Gravatar Arnaud Spiwack2014-10-16
* Proofview: small optimisation/simplification.Gravatar Arnaud Spiwack2014-10-16
* ConstructiveEpsilon: simplify the before_witness type using non-uniform param...Gravatar Arnaud Spiwack2014-10-16
* Adding a timeout to bug #2447.Gravatar Pierre-Marie Pédrot2014-10-15
* To stay closer to non-primitive projections, only unfold primitiveGravatar Matthieu Sozeau2014-10-15
* Make use of unfolded primitive projections when elaborating match on aGravatar Matthieu Sozeau2014-10-15
* Fix ill-typed debugging functionGravatar Matthieu Sozeau2014-10-15
* Fix for bug #3618.Gravatar Matthieu Sozeau2014-10-15
* Remaining tactics of the Auto module were put in the monad.Gravatar Pierre-Marie Pédrot2014-10-15
* Closed bug 3710.Gravatar Matthieu Sozeau2014-10-15
* Bug 3692 is fixed.Gravatar Matthieu Sozeau2014-10-15
* Bug 3628 is fixed.Gravatar Matthieu Sozeau2014-10-15
* Fix test-suite files which failed due to usage of $(admit)$ whichGravatar Matthieu Sozeau2014-10-15
* Fix bug 3637.Gravatar Matthieu Sozeau2014-10-15
* Reenable FO unification of primitive projections and their eta-expandedGravatar Matthieu Sozeau2014-10-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 17:09:52 +0000