aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fix English spelling -> American spelling in doc.Gravatar Arnaud Spiwack2014-08-01
* CHANGES: [numgoals] and [guard].Gravatar Arnaud Spiwack2014-08-01
* Document [numgoals] and [guard].Gravatar Arnaud Spiwack2014-08-01
* Add [guard] tactic.Gravatar Arnaud Spiwack2014-08-01
* Add [numgoal] to Ltac.Gravatar Arnaud Spiwack2014-08-01
* Add primtive [num_goal] to Proofview.Gravatar Arnaud Spiwack2014-08-01
* Untyped terms in ltac: simplify [coerce_to_uconstr].Gravatar Arnaud Spiwack2014-08-01
* Remove spurious [1] in equality.ml.Gravatar Arnaud Spiwack2014-08-01
* Clean outdated comment in Proofview.Notations.Gravatar Arnaud Spiwack2014-08-01
* Fix typo in cf04daec997.Gravatar Arnaud Spiwack2014-08-01
* micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)Gravatar Frédéric Besson2014-08-01
* Compatibility for compilation with ocaml 3.12 (at least).Gravatar Hugo Herbelin2014-08-01
* micromega : improve efficiency/termination of type-checkingGravatar Frédéric Besson2014-08-01
* Continuing (incomplete) cleaning of Inductiveops.Gravatar Hugo Herbelin2014-08-01
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Removing more tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
* Removing some tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
* Useless export of Instance.eqeq. We hashcons everything before calling thisGravatar Pierre-Marie Pédrot2014-07-31
* Making the error message about bullets more precise.Gravatar Pierre Courtieu2014-07-31
* Removing the call to Weak.get_copy in hashsets.Gravatar Pierre-Marie Pédrot2014-07-31
* micromega : refification recognises @eq T for T convertible with Z or RGravatar Frédéric Besson2014-07-31
* Typos.Gravatar Hugo Herbelin2014-07-31
* Finish fixes on notations and primitive projections, add test-suite files for...Gravatar Matthieu Sozeau2014-07-31
* Consistent pretty-printing of primitive projections and their expanded forms.Gravatar Matthieu Sozeau2014-07-31
* Add an option to solve typeclass goals generated by apply which can't beGravatar Matthieu Sozeau2014-07-31
* Adding a generalized version of fold_Equal to FMapFacts.Gravatar Pierre Courtieu2014-07-31
* Optimize check of new subterm relation on match.Gravatar Maxime Dénès2014-07-31
* Improve intersection of regular trees.Gravatar Maxime Dénès2014-07-31
* Fix dynamic computation of recargs for mutual inductives.Gravatar Maxime Dénès2014-07-31
* Add test-suite file for bug #3439.Gravatar Matthieu Sozeau2014-07-30
* Avoid hconsing instances during appends and conversions from/to arrays.Gravatar Matthieu Sozeau2014-07-30
* Fix discrimination net which was not recognizing primitive projections.Gravatar Matthieu Sozeau2014-07-30
* Avoid introducing additional universes when doing pruning in evarsolve.Gravatar Matthieu Sozeau2014-07-30
* CHANGES: untyped terms in tacticsGravatar Arnaud Spiwack2014-07-29
* Document untyped terms in tactics.Gravatar Arnaud Spiwack2014-07-29
* Small refactoring in Ltac parsing rules.Gravatar Arnaud Spiwack2014-07-29
* Allow [uconstr:c] as argument of a tactic.Gravatar Arnaud Spiwack2014-07-29
* Untyped terms in tactic: add the possibility to use a typed term inside an un...Gravatar Arnaud Spiwack2014-07-29
* Untyped terms in tactic: function [type_term c] to give a typed version of [c].Gravatar Arnaud Spiwack2014-07-29
* Untyped term in tactics: add an grammar entry to construct them.Gravatar Arnaud Spiwack2014-07-29
* Add a type of untyped term to Ltac's value.Gravatar Arnaud Spiwack2014-07-29
* Clean up obsolete comment.Gravatar Arnaud Spiwack2014-07-29
* Add test-suite file for bug 3454.Gravatar Matthieu Sozeau2014-07-29
* Rework code for refolding projections in whd_state/whd_simpl to allow ArgumentsGravatar Matthieu Sozeau2014-07-29
* Fix eta-conversion code which was failing in nested cases. Fixes bug #3429.Gravatar Matthieu Sozeau2014-07-29
* Add test-suite file for bug #3453Gravatar Matthieu Sozeau2014-07-29
* Fix bug #3453, not recognizing primitive projections in Coercion declarations.Gravatar Matthieu Sozeau2014-07-29
* Fix treatment of notations containing applications of projections (fixes bug ...Gravatar Matthieu Sozeau2014-07-29
* STM: print goals with no duplicatesGravatar Enrico Tassi2014-07-29
* Pp: only one default feedback idGravatar Enrico Tassi2014-07-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-02 17:17:10 +0000