aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* -help failing (fix 3762)Gravatar Enrico Tassi2014-10-24
* Fix typo in documentation of the [repeat] tactical.Gravatar Arnaud Spiwack2014-10-24
* No hash consing across calls to the native compiler.Gravatar Maxime Dénès2014-10-24
* Fixing order of declarations in the function which compacts variablesGravatar Hugo Herbelin2014-10-23
* Fixing clash in output test-suite Cases.Gravatar Hugo Herbelin2014-10-23
* Taking into account factorization of consecutive names of same typesGravatar Hugo Herbelin2014-10-23
* fix parsing of ---- +++++ ***** in CoqIDEGravatar Enrico Tassi2014-10-23
* Monad: change the error managing of two-list combinators.Gravatar Arnaud Spiwack2014-10-23
* Evd.future_goals: forgot to revert the list in two places.Gravatar Arnaud Spiwack2014-10-23
* Proofview: forgot to change an exception after refactoring in ( 9f51aafebd5f3...Gravatar Arnaud Spiwack2014-10-23
* Bugfix 3604 : more robust Unix.lockfGravatar Frédéric Besson2014-10-22
* Fixing typo in output test Notations.Gravatar Hugo Herbelin2014-10-22
* Pushing Pierre's factorization of names in goal context printing fromGravatar Hugo Herbelin2014-10-22
* Removing an unused variant of Context.fold_named_context_reverse.Gravatar Hugo Herbelin2014-10-22
* CoqIDE: fix parsing of multicharacter bulletsGravatar Enrico Tassi2014-10-22
* Specializing tclBREAK so that it can choose the return exception in caseGravatar Pierre-Marie Pédrot2014-10-22
* Make rint_location_in_file resilient to Cd (close 3630)Gravatar Enrico Tassi2014-10-22
* Fix the way lexeme start is computed (Close 3737)Gravatar Enrico Tassi2014-10-22
* Goal printing made uniform: always done in STM (close 3585)Gravatar Enrico Tassi2014-10-22
* Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)Gravatar Enrico Tassi2014-10-22
* Fix test-suite for #2729.Gravatar Maxime Dénès2014-10-22
* Fix missing lift in VM and native compiler (second part of #2729).Gravatar Maxime Dénès2014-10-22
* Refine tactic: simplify the conclusion only at the end of the tactic.Gravatar Arnaud Spiwack2014-10-22
* Oversight in ce260a0db279ce09dda70e079ae3c35b49f05ec4 (Proper scoping of futu...Gravatar Arnaud Spiwack2014-10-22
* Remove an unnecessary use of [Proofview.Unsafe.tclEVARS] in [convert_concl].Gravatar Arnaud Spiwack2014-10-22
* EqdepFacts: generalize statements which were wrongly restricted to Prop.Gravatar Arnaud Spiwack2014-10-22
* CHANGES: makes explicit the incompatibily introduced by the use of Ltac-defin...Gravatar Arnaud Spiwack2014-10-22
* Fixing an evar leak in pattern-matching compilation (#3758).Gravatar Hugo Herbelin2014-10-22
* Fixing what really looks like a bug in the initial implementation ofGravatar Hugo Herbelin2014-10-22
* Supporting Greek and Coptic (U0370) as first letter of coqdoc identifiers.Gravatar Hugo Herbelin2014-10-22
* Fixing typo absorption (bug #3751).Gravatar Hugo Herbelin2014-10-22
* Proofview: documentation and re-ordering.Gravatar Arnaud Spiwack2014-10-22
* Split [Proofview] into a file where the basic operations on the state are def...Gravatar Arnaud Spiwack2014-10-22
* Make names in [Proofview_monad] more uniform.Gravatar Arnaud Spiwack2014-10-22
* Proofview: remove and inline [on_advance] function.Gravatar Arnaud Spiwack2014-10-22
* Proofview: add a lens for the evar_map and factor some code.Gravatar Arnaud Spiwack2014-10-22
* Proofview: use an iter-like combinator rather than a fold_left-like one for d...Gravatar Arnaud Spiwack2014-10-22
* An additional [List.iter] monadic combinator.Gravatar Arnaud Spiwack2014-10-22
* Add more primitives to the [Monad.Make] arguments.Gravatar Arnaud Spiwack2014-10-22
* Improve readability the "lenses" in Proofview, using interfaces.Gravatar Arnaud Spiwack2014-10-22
* Proofview: clean up code a little.Gravatar Arnaud Spiwack2014-10-22
* Proofview: move [list_goto] to the [CList] module.Gravatar Arnaud Spiwack2014-10-22
* Proofview: replace the functions iter_list and iter_list2 by generic monadic ...Gravatar Arnaud Spiwack2014-10-22
* Add a two-list monadic fold_left iterator.Gravatar Arnaud Spiwack2014-10-22
* Small optimisation in the monadic list combinators.Gravatar Arnaud Spiwack2014-10-22
* Factor module signatures.Gravatar Arnaud Spiwack2014-10-22
* Proofview: clean up commented out code.Gravatar Arnaud Spiwack2014-10-22
* Proofview: remove a redundant primitive.Gravatar Arnaud Spiwack2014-10-22
* Proofview: move more functions to the Unsafe module.Gravatar Arnaud Spiwack2014-10-22
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 21:37:44 +0000