aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-08-01CHANGES: [>…].Arnaud Spiwack
2014-08-01Document [> … ].Arnaud Spiwack
2014-08-01New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.Arnaud Spiwack
2014-08-01Fix English spelling -> American spelling in doc.Arnaud Spiwack
2014-08-01CHANGES: [numgoals] and [guard].Arnaud Spiwack
2014-08-01Document [numgoals] and [guard].Arnaud Spiwack
2014-08-01Add [guard] tactic.Arnaud Spiwack
2014-08-01Add [numgoal] to Ltac.Arnaud Spiwack
2014-08-01Add primtive [num_goal] to Proofview.Arnaud Spiwack
2014-08-01Untyped terms in ltac: simplify [coerce_to_uconstr].Arnaud Spiwack
2014-08-01Remove spurious [1] in equality.ml.Arnaud Spiwack
2014-08-01Clean outdated comment in Proofview.Notations.Arnaud Spiwack
2014-08-01Fix typo in cf04daec997.Arnaud Spiwack
2014-08-01micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)Frédéric Besson
2014-08-01Compatibility for compilation with ocaml 3.12 (at least).Hugo Herbelin
2014-08-01micromega : improve efficiency/termination of type-checkingFrédéric Besson
2014-08-01Continuing (incomplete) cleaning of Inductiveops.Hugo Herbelin
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-08-01Removing more tactic compatibility layer.Pierre-Marie Pédrot
2014-08-01Removing some tactic compatibility layer.Pierre-Marie Pédrot
2014-07-31Useless export of Instance.eqeq. We hashcons everything before calling thisPierre-Marie Pédrot
2014-07-31Making the error message about bullets more precise.Pierre Courtieu
2014-07-31Removing the call to Weak.get_copy in hashsets.Pierre-Marie Pédrot
2014-07-31micromega : refification recognises @eq T for T convertible with Z or RFrédéric Besson
2014-07-31Typos.Hugo Herbelin
2014-07-31Finish fixes on notations and primitive projections, add test-suite files for...Matthieu Sozeau
2014-07-31Consistent pretty-printing of primitive projections and their expanded forms.Matthieu Sozeau
2014-07-31Add an option to solve typeclass goals generated by apply which can't beMatthieu Sozeau
2014-07-31Adding a generalized version of fold_Equal to FMapFacts.Pierre Courtieu
2014-07-31Optimize check of new subterm relation on match.Maxime Dénès
2014-07-31Improve intersection of regular trees.Maxime Dénès
2014-07-31Fix dynamic computation of recargs for mutual inductives.Maxime Dénès
2014-07-30Add test-suite file for bug #3439.Matthieu Sozeau
2014-07-30Avoid hconsing instances during appends and conversions from/to arrays.Matthieu Sozeau
2014-07-30Fix discrimination net which was not recognizing primitive projections.Matthieu Sozeau
2014-07-30Avoid introducing additional universes when doing pruning in evarsolve.Matthieu Sozeau
2014-07-29CHANGES: untyped terms in tacticsArnaud Spiwack
2014-07-29Document untyped terms in tactics.Arnaud Spiwack
2014-07-29Small refactoring in Ltac parsing rules.Arnaud Spiwack
2014-07-29Allow [uconstr:c] as argument of a tactic.Arnaud Spiwack
2014-07-29Untyped terms in tactic: add the possibility to use a typed term inside an un...Arnaud Spiwack
2014-07-29Untyped terms in tactic: function [type_term c] to give a typed version of [c].Arnaud Spiwack
2014-07-29Untyped term in tactics: add an grammar entry to construct them.Arnaud Spiwack
2014-07-29Add a type of untyped term to Ltac's value.Arnaud Spiwack
2014-07-29Clean up obsolete comment.Arnaud Spiwack
2014-07-29Add test-suite file for bug 3454.Matthieu Sozeau
2014-07-29Rework code for refolding projections in whd_state/whd_simpl to allow ArgumentsMatthieu Sozeau
2014-07-29Fix eta-conversion code which was failing in nested cases. Fixes bug #3429.Matthieu Sozeau
2014-07-29Add test-suite file for bug #3453Matthieu Sozeau
2014-07-29Fix bug #3453, not recognizing primitive projections in Coercion declarations.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 21:42:00 +0000