aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Proofview.mli: no more reference to Goal.goal.Gravatar Arnaud Spiwack2014-10-22
* Proofview: factor init and dependent_init.Gravatar Arnaud Spiwack2014-10-22
* Remove unused functions for side effects.Gravatar Arnaud Spiwack2014-10-22
* Remove the deprecated open-constr based refine.Gravatar Arnaud Spiwack2014-10-22
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
* Remove duplicate code.Gravatar Arnaud Spiwack2014-10-22
* Removing dead code in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
* Small invariants in Rewrite code.Gravatar Pierre-Marie Pédrot2014-10-21
* Lazily check that an argument is dependent when constructing evar clauses.Gravatar Pierre-Marie Pédrot2014-10-21
* Fixing decompose_app_rel in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
* Using new clausenv in rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
* Adding an evar version of the make_clenv function.Gravatar Pierre-Marie Pédrot2014-10-21
* Porting Hugo's fix 98f3abb83a to native compiler.Gravatar Maxime Dénès2014-10-21
* Adapting output tests to the removal of the new token warning and toGravatar Hugo Herbelin2014-10-21
* More precise test for #3459.Gravatar Hugo Herbelin2014-10-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-17 00:32:20 +0000