aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2018-02-20Make pattern variables of "match" substitutable in notations.Hugo Herbelin
2018-02-20Supporting recursive notations reversing the left-to-right order.Hugo Herbelin
2018-02-20Allowing variables used in recursive notation to occur several times in pattern.Hugo Herbelin
2018-02-20Allows recursive patterns for binders to be associative on the left.Hugo Herbelin
2018-02-20Fixing/improving notations with recursive patterns.Hugo Herbelin
2018-02-20A bit of miscellaneous code documentation around notations.Hugo Herbelin
2018-02-20Notations: documenting structure collecting variables occurring in notation.Hugo Herbelin
2018-02-20Minor clarifying of name variables in constrintern.ml.Hugo Herbelin
2018-02-20Using name given by user to name a 'pat, if any.Hugo Herbelin
2018-02-20Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Hugo Herbelin
2018-02-20Notations: Do not consider a non-occurring variable as a binder-only variable.Hugo Herbelin
2018-02-20More precise explanation when a notation is not reversible for printing.Hugo Herbelin
2018-02-20Adding support for re-folding notation referring to isolated "forall '(x,y), t".Hugo Herbelin
2018-02-20Again one more step in fixing #5762 ("where" clause).Hugo Herbelin
2018-02-16Extrude monomorphic universe contexts from with Definition constraints.Pierre-Marie Pédrot
2018-02-12Merge PR #1047: Support universe instances on the literal TypeMaxime Dénès
2018-02-12Merge PR #6128: Simplification: cumulativity information is variance informa...Maxime Dénès
2018-02-11Use specialized function for inductive subtyping inference.Gaëtan Gilbert
2018-02-10Inference of inductive subtyping does not need an evar map.Gaëtan Gilbert
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
2018-01-30Use r.(p) syntax to print primitive projections.Maxime Dénès
2018-01-26Support universe instances on the literal TypeTej Chajed
2018-01-08Merge PR #6532: Fix mli-doc issue #6531Maxime Dénès
2018-01-01Fix mli-doc issue #6531Tony Beta Lambda
2017-12-30Using a dedicated type for Lib.abstr_info.Pierre-Marie Pédrot
2017-12-27Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.Maxime Dénès
2017-12-27Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...Maxime Dénès
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-12-22Merge PR #6469: No universe constraints in Let definitionsMaxime Dénès
2017-12-20Merge PR #6449: Let definitions must not contain side-effects when reaching t...Maxime Dénès
2017-12-19Let definitions do not create new universe constraints.Pierre-Marie Pédrot
2017-12-19Specific type for section definition entries.Pierre-Marie Pédrot
2017-12-18Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Maxime Dénès
2017-12-16Let definitions must not contain side-effects when reaching the kernel.Pierre-Marie Pédrot
2017-12-15Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Maxime Dénès
2017-12-15[econstr] Switch constrintern API to non-imperative style.Emilio Jesus Gallego Arias
2017-12-14Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...Maxime Dénès
2017-12-13[econstr] Cleanup in `vernac/classes.ml`.Emilio Jesus Gallego Arias
2017-12-12In printing, factorizing "match" clauses with same right-hand side.Hugo Herbelin
2017-12-12Removing cumbersome location in multiple patterns.Hugo Herbelin
2017-12-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-12-07Merge PR #873: New strategy based on open scopes for deciding which notation ...Maxime Dénès
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
2017-11-30Remove unused boolean from cl_context field of Typeclasses.typeclassGaëtan Gilbert
2017-11-29Remove "obsolete_locality" and fix STM vernac classification.Maxime Dénès
2017-11-27Selecting which notation to print based on current stack of scope.Hugo Herbelin
2017-11-24Use Entries.constant_universes_entry more.Gaëtan Gilbert
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
2017-11-24Stop exposing UState.universe_context and its Evd wrapper.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 07:52:29 +0000