aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-09-05Adding a Ftactic module for potentially focussing tactics.Pierre-Marie Pédrot
2014-09-05Removing the old implementation of clear_body.Pierre-Marie Pédrot
2014-09-05Fix primitive projections declarations for inductive records.Matthieu Sozeau
2014-09-05At last a working clearbody!Pierre-Marie Pédrot
2014-09-04Only using filtered hyps in Goal.enter.Pierre-Marie Pédrot
2014-09-04Ensuring the invariant that hypotheses and named context of the environment ofPierre-Marie Pédrot
2014-09-04Revert the two previous commits. I was testing in the wrong branch.Pierre-Marie Pédrot
2014-09-04Removing the old implementation of clear_body.Pierre-Marie Pédrot
2014-09-04Reimplementing the clearbody tactic.Pierre-Marie Pédrot
2014-09-04Make CoqIDE compile with windows (Closes: 3573)Enrico Tassi
2014-09-04Fix: shelve_unifiable did not work modulo evar instantiation.Arnaud Spiwack
2014-09-04Proofview refiner is now type-safe by default.Pierre-Marie Pédrot
2014-09-04Typing.sort_of does not leak evarmaps anymore.Pierre-Marie Pédrot
2014-09-04More explicit printing in Himsg.Pierre-Marie Pédrot
2014-09-04Status error for bug #3459.Pierre-Marie Pédrot
2014-09-04Test for bug #3459.Pierre-Marie Pédrot
2014-09-04Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Pierre-Marie Pédrot
2014-09-04Using goal-tactics to interpret arguments to idtac.Pierre-Marie Pédrot
2014-09-04Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."Pierre-Marie Pédrot
2014-09-04Revert "Tacinterp: [interp_message] and associate now only require an environ...Pierre-Marie Pédrot
2014-09-04Revert "Ltac's idtac is now implemented using the new API."Pierre-Marie Pédrot
2014-09-04Revert "Ltac's [idtac] is now interpreted outside of a goal if possible."Pierre-Marie Pédrot
2014-09-04Fix bug #3561, correct folding of env in context[] matching.Matthieu Sozeau
2014-09-04Fix bug #3559, ensuring a canonical order of universe level quantifications whenMatthieu Sozeau
2014-09-04Documenting the [Variant] type definition and the [Nonrecursive Elimination S...Arnaud Spiwack
2014-09-04Commands like [Inductive > X := … | … | …] raise an error message inste...Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-14 09:45:26 +0000