aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2021-03-30[flags] [profile] Remove bit-rotten CProfile code.Emilio Jesus Gallego Arias
2021-03-26[doc] cleanup pretyping/structures.mliEnrico Tassi
2021-03-26[recordops] complete API rewrite; the module is now called [structures]Enrico Tassi
2021-03-25Merge PR #13909: Minimize the set of multiple inheritance (coercion) paths to...coqbot-app[bot]
2021-03-26Expose less interface in coercionops.mliKazuhiko Sakaguchi
2021-03-12Move the responsibility of type-checking to the caller for tactic-in-terms.Pierre-Marie Pédrot
2021-03-13Minimize the set of multiple inheritance paths to check for conversionKazuhiko Sakaguchi
2021-03-11Merge PR #13854: Normalize evars during bytecode compilation.coqbot-app[bot]
2021-03-09Add the source and target classes to the coercion tableKazuhiko Sakaguchi
2021-03-09Replace cl_index with cl_typ in coercionops.mlKazuhiko Sakaguchi
2021-03-06Merge PR #13902: [coercion] expose coercion_infoPierre-Marie Pédrot
2021-03-05[coercipn] expose coercion_infoEnrico Tassi
2021-03-03Merge PR #12567: [build] Split stdlib to it's own package.coqbot-app[bot]
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-03-02Merge PR #13889: Dead code elimination: not reducible error message is never ...coqbot-app[bot]
2021-03-02Dead code elimination: not reducible error message is never raised.Théo Zimmermann
2021-02-28Merge PR #13853: Delay the dynamic linking of native-code libraries until nat...Pierre-Marie Pédrot
2021-02-26Merge PR #13869: Use make_case_or_project in auto_ind_declPierre-Marie Pédrot
2021-02-26Delay the dynamic linking of native-code libraries until native_compute is ca...Guillaume Melquiond
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-24Use Reductionops.clos_whd_flags in vm_compute and native_compute.Guillaume Melquiond
2021-02-23Normalize evars during bytecode compilation (fix #13841).Guillaume Melquiond
2021-02-22Merge PR #13836: Make detyping more resistent in the debuggerPierre-Marie Pédrot
2021-02-17Use make_case_or_project in auto_ind_declGaëtan Gilbert
2021-02-17Merge PR #13734: Fix #13732: Implicit Type vs universesPierre-Marie Pédrot
2021-02-08Make detyping more resistent in the debuggerGaëtan Gilbert
2021-01-20Slightly less stupid algorithm for simpl fixpoint expansion.Pierre-Marie Pédrot
2021-01-20Inline the function in contract_[co]fix_use_function.Pierre-Marie Pédrot
2021-01-20Factorize the call of nf_beta in red_elim_const.Pierre-Marie Pédrot
2021-01-20Merge PR #13721: Remove strong reduction wrapperscoqbot-app[bot]
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
2021-01-18Merge PR #13723: Use a compact case representation for patternscoqbot-app[bot]
2021-01-18Do not call the with_full_binder map variant for Reduction.instance.Pierre-Marie Pédrot
2021-01-18Move the two only calls to the strong combinator to their calling site.Pierre-Marie Pédrot
2021-01-18Move the only use of strong_with_flags to its single calling module.Pierre-Marie Pédrot
2021-01-18Fix #13579 (hnf on primitives raises an anomaly)Pierre Roux
2021-01-12Same treatment for pattern functions used by rewrite.Pierre-Marie Pédrot
2021-01-12Extrude the check for pattern groundness outside of unification.Pierre-Marie Pédrot
2021-01-12Restore the corner-case behaviour for let-bound variables in patterns.Pierre-Marie Pédrot
2021-01-12Slight tweak of the matching algorithm for PIf vs. Case.Pierre-Marie Pédrot
2021-01-12Change the case representation of patterns.Pierre-Marie Pédrot
2021-01-11Respect print_universes in detype_instanceGaëtan Gilbert
2021-01-04Try to preserve the old unification behaviour w.r.t. let-ins in branches.Pierre-Marie Pédrot
2021-01-04Make detyping more robust w.r.t. case representation.Pierre-Marie Pédrot
2021-01-04Remove redundant univ and parameter info from CaseInvertGaëtan Gilbert
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
2020-12-21Remove the artificial dependency of Heads on evaluable_global_reference.Pierre-Marie Pédrot
2020-12-20Merge PR #13138: Towards a documentation / cleanup of evarconvcoqbot-app[bot]
2020-12-18Merge PR #13628: Cache meta instances in Clenvcoqbot-app[bot]
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:47:35 +0000