aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Fix bug #3559, ensuring a canonical order of universe level quantifications whenGravatar Matthieu Sozeau2014-09-04
* Documenting the [Variant] type definition and the [Nonrecursive Elimination S...Gravatar Arnaud Spiwack2014-09-04
* Commands like [Inductive > X := … | … | …] raise an error message inste...Gravatar Arnaud Spiwack2014-09-04
* Factorize the parsing rules of [Record] and the other kind of type definitions.Gravatar Arnaud Spiwack2014-09-04
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
* Type definitions with [Variant] don't generate inductive schemes by default.Gravatar Arnaud Spiwack2014-09-04
* Type definitions [Variant] and [Record] really don't accept the wrong kind of...Gravatar Arnaud Spiwack2014-09-04
* Inductive and CoInductive records are printed correctly.Gravatar Arnaud Spiwack2014-09-04
* Types declared as Variants really do not accept recursive definitions.Gravatar Arnaud Spiwack2014-09-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 17:26:13 +0000