aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2019-02-08Coercion intf fixMatthieu Sozeau
2019-02-08Fix issue found in GeoCoqMatthieu Sozeau
2019-02-08Add back the deprecated conv/cumul functions.Matthieu Sozeau
2019-02-08Document the unify_flags more throroughly in evarsolve.Matthieu Sozeau
2019-02-08[evarconv] Handle frozen evars in solve_unif_constraints_with_heuristicsMatthieu Sozeau
2019-02-08[evarconv] Clean second order matching of evdrefsMatthieu Sozeau
2019-02-08Change interfaces of evarconv as suggested by Enrico.Matthieu Sozeau
2019-02-08print_constr_env moved to Internal moduleMatthieu Sozeau
2019-02-08Fix warning unused variableMatthieu Sozeau
2019-02-08[occur_rigidly] Try improving occur-check approximationMatthieu Sozeau
2019-02-08Add an helper [instantiate_evar] functionMatthieu Sozeau
2019-02-08Flags of evar_conv_x/unifiers: rationalizeMatthieu Sozeau
2019-02-08Rename types_or_terms and the unification function typesMatthieu Sozeau
2019-02-08Correct occur_rigidlyMatthieu Sozeau
2019-02-08Abstraction namingMatthieu Sozeau
2019-02-08unification: abstract_list_all_with_dependencies fixMatthieu Sozeau
2019-02-08evarconv/evarsolve: HO matching algorithm with occurrence selectionMatthieu Sozeau
2019-02-08[evarconv] New flag handling for unifierMatthieu Sozeau
2019-02-08locus: Add an AtLeastOneOccurrence constructor.Matthieu Sozeau
2019-02-08Evd/evarsolve: add an abstraction field to evars for unificationMatthieu Sozeau
2019-02-08Merge PR #9410: Make `Program` a regular attributeMatthieu Sozeau
2019-02-05Merge PR #9397: Simplify code for Recordops.cs_pattern_of_constrMatthieu Sozeau
2019-02-05Make Program a regular attributeMaxime Dénès
2019-02-04Merge PR #6914: Primitive integersPierre-Marie Pédrot
2019-02-04Merge PR #9144: Fixes #4633: clearer message unknown existentialPierre-Marie Pédrot
2019-02-04Primitive integersMaxime Dénès
2019-02-04Merge PR #9368: Discard argument names of section variables on section closePierre-Marie Pédrot
2019-01-24Simplify code for Recordops.cs_pattern_of_constrGaëtan Gilbert
2019-01-22[CS] recognize applied primitive projections as keys (fix #9375)Enrico Tassi
2019-01-20Discard argument names of section variables on section closeJasper Hugunin
2019-01-10Remove Printing Primitive Projection CompatibilityGaëtan Gilbert
2019-01-06Fixes #4633: more explicit error message when referring to a generated evar.Hugo Herbelin
2019-01-06Renaming pr_evar_suggested_name into -> evar_suggested_name.Hugo Herbelin
2018-12-21Fix #9240: Register for IDProp causes anomaly when non constantGaëtan Gilbert
2018-12-18[arguments] cleanupEnrico Tassi
2018-12-12Higher-level libobject API for objects with fixed scopesMaxime Dénès
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-12Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comme...Maxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-12-06Revise API for global universes.Gaëtan Gilbert
2018-12-06Fix race condition triggered by fresh universe generationMaxime Dénès
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-11-28Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a classMatthieu Sozeau
2018-11-28[options] New helper for creation of boolean options plus reference.Emilio Jesus Gallego Arias
2018-11-27Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...Emilio Jesus Gallego Arias
2018-11-27Merge PR #7696: Remove some univ_flexible_alg from casesPierre-Marie Pédrot
2018-11-27Merge PR #8255: Fast typing of application nodesMaxime Dénès
2018-11-27[Typeclasses] Warn when RHS of `:>` is not a classVincent Laporte
2018-11-24Merge PR #8929: Fix fixpoint related lifting in open recursors + related clea...Pierre-Marie Pédrot
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:56:55 +0000