aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-10-22Fix test-suite for #2729.Maxime Dénès
2014-10-22Fix missing lift in VM and native compiler (second part of #2729).Maxime Dénès
2014-10-22Refine tactic: simplify the conclusion only at the end of the tactic.Arnaud Spiwack
2014-10-22Oversight in ce260a0db279ce09dda70e079ae3c35b49f05ec4 (Proper scoping of futu...Arnaud Spiwack
2014-10-22Remove an unnecessary use of [Proofview.Unsafe.tclEVARS] in [convert_concl].Arnaud Spiwack
2014-10-22EqdepFacts: generalize statements which were wrongly restricted to Prop.Arnaud Spiwack
2014-10-22CHANGES: makes explicit the incompatibily introduced by the use of Ltac-defin...Arnaud Spiwack
2014-10-22Fixing an evar leak in pattern-matching compilation (#3758).Hugo Herbelin
2014-10-22Fixing what really looks like a bug in the initial implementation ofHugo Herbelin
2014-10-22Supporting Greek and Coptic (U0370) as first letter of coqdoc identifiers.Hugo Herbelin
2014-10-22Fixing typo absorption (bug #3751).Hugo Herbelin
2014-10-22Proofview: documentation and re-ordering.Arnaud Spiwack
2014-10-22Split [Proofview] into a file where the basic operations on the state are def...Arnaud Spiwack
2014-10-22Make names in [Proofview_monad] more uniform.Arnaud Spiwack
2014-10-22Proofview: remove and inline [on_advance] function.Arnaud Spiwack
2014-10-22Proofview: add a lens for the evar_map and factor some code.Arnaud Spiwack
2014-10-22Proofview: use an iter-like combinator rather than a fold_left-like one for d...Arnaud Spiwack
2014-10-22An additional [List.iter] monadic combinator.Arnaud Spiwack
2014-10-22Add more primitives to the [Monad.Make] arguments.Arnaud Spiwack
2014-10-22Improve readability the "lenses" in Proofview, using interfaces.Arnaud Spiwack
2014-10-22Proofview: clean up code a little.Arnaud Spiwack
2014-10-22Proofview: move [list_goto] to the [CList] module.Arnaud Spiwack
2014-10-22Proofview: replace the functions iter_list and iter_list2 by generic monadic ...Arnaud Spiwack
2014-10-22Add a two-list monadic fold_left iterator.Arnaud Spiwack
2014-10-22Small optimisation in the monadic list combinators.Arnaud Spiwack
2014-10-22Factor module signatures.Arnaud Spiwack
2014-10-22Proofview: clean up commented out code.Arnaud Spiwack
2014-10-22Proofview: remove a redundant primitive.Arnaud Spiwack
2014-10-22Proofview: move more functions to the Unsafe module.Arnaud Spiwack
2014-10-22Proofview: split [V82] module into [Unsafe] and [V82].Arnaud Spiwack
2014-10-22Proofview.mli: no more reference to Goal.goal.Arnaud Spiwack
2014-10-22Proofview: factor init and dependent_init.Arnaud Spiwack
2014-10-22Remove unused functions for side effects.Arnaud Spiwack
2014-10-22Remove the deprecated open-constr based refine.Arnaud Spiwack
2014-10-22Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Arnaud Spiwack
2014-10-22Remove duplicate code.Arnaud Spiwack
2014-10-21Removing dead code in Rewrite.Pierre-Marie Pédrot
2014-10-21Small invariants in Rewrite code.Pierre-Marie Pédrot
2014-10-21Lazily check that an argument is dependent when constructing evar clauses.Pierre-Marie Pédrot
2014-10-21Fixing decompose_app_rel in Rewrite.Pierre-Marie Pédrot
2014-10-21Using new clausenv in rewrite.Pierre-Marie Pédrot
2014-10-21Adding an evar version of the make_clenv function.Pierre-Marie Pédrot
2014-10-21Porting Hugo's fix 98f3abb83a to native compiler.Maxime Dénès
2014-10-21Adapting output tests to the removal of the new token warning and toHugo Herbelin
2014-10-21More precise test for #3459.Hugo Herbelin
2014-10-21Dead code.Hugo Herbelin
2014-10-21Continuing experimental printing of the signature of open evars inHugo Herbelin
2014-10-20Removing re-typecheking from "refine" in no-check mode of the newHugo Herbelin
2014-10-20Fixing a (new) part of bug #2729.Hugo Herbelin
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 16:24:49 +0000