aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-09-08Removing antiquotations in Tauto.Pierre-Marie Pédrot
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-09-08Removing the documentation of the XML plugin.Pierre-Marie Pédrot
2014-09-08Removing the XML plugin.Pierre-Marie Pédrot
2014-09-08Fix bug #3591: print differently eta-expanded projection implicit application...Matthieu Sozeau
2014-09-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
2014-09-08Display number of available goals in "incorrect number of goals" error message.Arnaud Spiwack
2014-09-08CHANGES: existential variables are always "substituted" in the new tactic eng...Arnaud Spiwack
2014-09-08CHANGES: Ltac's [refine] accepts [uconstr].Arnaud Spiwack
2014-09-08Doc: [revgoals].Arnaud Spiwack
2014-09-08CHANGES: [revgoals].Arnaud Spiwack
2014-09-08Fix [induction] wrt inductive records and non-recursive variants.Arnaud Spiwack
2014-09-08CHANGES: [Variant], [Set Nonrecursive Elimination Schemes].Arnaud Spiwack
2014-09-08CHANGES: binder names from Ltac identifiers.Arnaud Spiwack
2014-09-08Rename [extract_ltac_uconstr_values] to [extract_ltac_constr_context].Arnaud Spiwack
2014-09-08The [constr:(…)] Ltac construction now shares the same context as [uconstr:...Arnaud Spiwack
2014-09-08Add a tactic [revgoals] to reverse the list of focused goals.Arnaud Spiwack
2014-09-08Fix bug #3589, unification looping due to incorrect use of stack with primiti...Matthieu Sozeau
2014-09-07Little fix in documentation of inversion.Hugo Herbelin
2014-09-07Test for "inversion as" naming bug.Hugo Herbelin
2014-09-07A better check that an "as" clause has been given to inversion, soHugo Herbelin
2014-09-07Fixing a bug in intros_replacing which was causing inversion notHugo Herbelin
2014-09-07Fixing "simple inversion as" (bug #2164).Hugo Herbelin
2014-09-07Dead code in inv.ml.Hugo Herbelin
2014-09-07Regression test #3557Hugo Herbelin
2014-09-07Regression test for bug #2883.Hugo Herbelin
2014-09-07Fixing bug #3492.Pierre-Marie Pédrot
2014-09-06Inlining code in Tacinterp that was only used once.Pierre-Marie Pédrot
2014-09-06Code simplification in Tacinterp.Pierre-Marie Pédrot
2014-09-06Proper interpretation function for tauto.Pierre-Marie Pédrot
2014-09-06Adding a way to inject tactic closures in interpretation values.Pierre-Marie Pédrot
2014-09-06Fixing clearbody : typecheck definitions in context.Pierre-Marie Pédrot
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-09-06Fix bug #3584, elaborating pattern-matching on primitive records to theMatthieu Sozeau
2014-09-06Remove debug printing codeMatthieu Sozeau
2014-09-06Cleanup code for looking up projection bodies.Matthieu Sozeau
2014-09-06Fix checker to handle projections with eta and universe polymorphism correctly,Matthieu Sozeau
2014-09-06Fix checker to handle projections with eta and universe polymorphism correctly.Matthieu Sozeau
2014-09-06Fix checking of constants in checker. Prelude can now be checked.Matthieu Sozeau
2014-09-05Remove unused substitution functions in checker.Matthieu Sozeau
2014-09-05Fix checker treatment of inductives using subst_instances instead of subst_un...Matthieu Sozeau
2014-09-05Retype terms resulting from the feeding of a context with a term.Pierre-Marie Pédrot
2014-09-05Fix checker/values.ml with latest changes due to projections and universes.Matthieu Sozeau
2014-09-05Remove a redundant typing phase in the [refine] tactic.Arnaud Spiwack
2014-09-05Silence an ocaml warning.Arnaud Spiwack
2014-09-05The pretyping of [uconstr] in [refine] uses the identifier of the ltac contex...Arnaud Spiwack
2014-09-05Ltac's [uconstr] values now use the identifier context to give names to binders.Arnaud Spiwack
2014-09-05Adds an identifier context in pretying's Ltac context.Arnaud Spiwack
2014-09-05Fix parsing of "subterm(s)" strategy argument.Matthieu Sozeau
2014-09-05Rename eta_expand_ind_stacks, fix the one from the checker and adaptMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 21:59:49 +0000