aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Dead code in inv.ml.Gravatar Hugo Herbelin2014-09-07
* Regression test #3557Gravatar Hugo Herbelin2014-09-07
* Regression test for bug #2883.Gravatar Hugo Herbelin2014-09-07
* Fixing bug #3492.Gravatar Pierre-Marie Pédrot2014-09-07
* Inlining code in Tacinterp that was only used once.Gravatar Pierre-Marie Pédrot2014-09-06
* Code simplification in Tacinterp.Gravatar Pierre-Marie Pédrot2014-09-06
* Proper interpretation function for tauto.Gravatar Pierre-Marie Pédrot2014-09-06
* Adding a way to inject tactic closures in interpretation values.Gravatar Pierre-Marie Pédrot2014-09-06
* Fixing clearbody : typecheck definitions in context.Gravatar Pierre-Marie Pédrot2014-09-06
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Fix bug #3584, elaborating pattern-matching on primitive records to theGravatar Matthieu Sozeau2014-09-06
* Remove debug printing codeGravatar Matthieu Sozeau2014-09-06
* Cleanup code for looking up projection bodies.Gravatar Matthieu Sozeau2014-09-06
* Fix checker to handle projections with eta and universe polymorphism correctly,Gravatar Matthieu Sozeau2014-09-06
* Fix checker to handle projections with eta and universe polymorphism correctly.Gravatar Matthieu Sozeau2014-09-06
* Fix checking of constants in checker. Prelude can now be checked.Gravatar Matthieu Sozeau2014-09-06
* Remove unused substitution functions in checker.Gravatar Matthieu Sozeau2014-09-05
* Fix checker treatment of inductives using subst_instances instead of subst_un...Gravatar Matthieu Sozeau2014-09-05
* Retype terms resulting from the feeding of a context with a term.Gravatar Pierre-Marie Pédrot2014-09-05
* Fix checker/values.ml with latest changes due to projections and universes.Gravatar Matthieu Sozeau2014-09-05
* Remove a redundant typing phase in the [refine] tactic.Gravatar Arnaud Spiwack2014-09-05
* Silence an ocaml warning.Gravatar Arnaud Spiwack2014-09-05
* The pretyping of [uconstr] in [refine] uses the identifier of the ltac contex...Gravatar Arnaud Spiwack2014-09-05
* Ltac's [uconstr] values now use the identifier context to give names to binders.Gravatar Arnaud Spiwack2014-09-05
* Adds an identifier context in pretying's Ltac context.Gravatar Arnaud Spiwack2014-09-05
* Fix parsing of "subterm(s)" strategy argument.Gravatar Matthieu Sozeau2014-09-05
* Rename eta_expand_ind_stacks, fix the one from the checker and adaptGravatar Matthieu Sozeau2014-09-05
* Adding a Ftactic module for potentially focussing tactics.Gravatar Pierre-Marie Pédrot2014-09-05
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-05
* Fix primitive projections declarations for inductive records.Gravatar Matthieu Sozeau2014-09-05
* At last a working clearbody!Gravatar Pierre-Marie Pédrot2014-09-05
* Only using filtered hyps in Goal.enter.Gravatar Pierre-Marie Pédrot2014-09-04
* Ensuring the invariant that hypotheses and named context of the environment ofGravatar Pierre-Marie Pédrot2014-09-04
* Revert the two previous commits. I was testing in the wrong branch.Gravatar Pierre-Marie Pédrot2014-09-04
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-04
* Reimplementing the clearbody tactic.Gravatar Pierre-Marie Pédrot2014-09-04
* Make CoqIDE compile with windows (Closes: 3573)Gravatar Enrico Tassi2014-09-04
* Fix: shelve_unifiable did not work modulo evar instantiation.Gravatar Arnaud Spiwack2014-09-04
* Proofview refiner is now type-safe by default.Gravatar Pierre-Marie Pédrot2014-09-04
* Typing.sort_of does not leak evarmaps anymore.Gravatar Pierre-Marie Pédrot2014-09-04
* More explicit printing in Himsg.Gravatar Pierre-Marie Pédrot2014-09-04
* Status error for bug #3459.Gravatar Pierre-Marie Pédrot2014-09-04
* Test for bug #3459.Gravatar Pierre-Marie Pédrot2014-09-04
* Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Gravatar Pierre-Marie Pédrot2014-09-04
* Using goal-tactics to interpret arguments to idtac.Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Tacinterp: [interp_message] and associate now only require an environ...Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Ltac's idtac is now implemented using the new API."Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Ltac's [idtac] is now interpreted outside of a goal if possible."Gravatar Pierre-Marie Pédrot2014-09-04
* Fix bug #3561, correct folding of env in context[] matching.Gravatar Matthieu Sozeau2014-09-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-12 22:53:53 +0000