aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2018-04-26Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.Hugo Herbelin
2018-04-26[api] Move `hint_info_expr` to `Typeclasses`.Emilio Jesus Gallego Arias
2018-04-26Always print explanation for univ inconsistency, rm Flags.univ_printGaëtan Gilbert
2018-04-23[api] Relocate `intf` modules according to dependency-order.Emilio Jesus Gallego Arias
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-04-13Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contain...Pierre-Marie Pédrot
2018-04-12Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Maxime Dénès
2018-04-10Replace uses of Termops.dependent by more specific functions.Pierre-Marie Pédrot
2018-04-10Do not compute constr matching context if not used.Pierre-Marie Pédrot
2018-04-08Fixes #7195 (missing freshness condition in Ltac pattern-matching names).Hugo Herbelin
2018-04-06Fix #5539: algebraic universe produced by cases.Gaëtan Gilbert
2018-04-01Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)Pierre-Marie Pédrot
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-28Supporting fix/cofix in Ltac pattern-matching (wish #7092).Hugo Herbelin
2018-03-28Patterns: Accepting patterns in PFix and PCofix and not only constr.Hugo Herbelin
2018-03-28Detyping: Adding a variant of share_names for patterns.Hugo Herbelin
2018-03-28Detyping: Making detype_fix/detype_cofix polymorphic combinator (step 1).Hugo Herbelin
2018-03-28Patternops: renaming an internal function to more closely match its effect.Hugo Herbelin
2018-03-28Glob_ops: cosmetic renaming to reflect the type of objects.Hugo Herbelin
2018-03-28Getting rid of some false "collision between bound variable names" warnings.Hugo Herbelin
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-03-27Fixing #5547 (typability of return predicate in nested pattern-matching).Hugo Herbelin
2018-03-27Fixing #5500 (missing test in return clause of match leading to anomaly).Hugo Herbelin
2018-03-26Fixes #7011 (Fix/CoFix were not considered in tactic unification).Hugo Herbelin
2018-03-24Slightly refining some error messages about unresolvable evars.Hugo Herbelin
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-09Merge PR #6775: Allow using cumulativity without forcing strict constraints.Maxime Dénès
2018-03-09Merge PR #6806: Adding missing unification constraint noticed by @skyskimmerMaxime Dénès
2018-03-09Merge PR #6769: Split closure cache and remove whd_bothMaxime Dénès
2018-03-09Delayed weak constraints for cumulative inductive types.Gaëtan Gilbert
2018-03-09Statically enforce that ULub is only between levels.Gaëtan Gilbert
2018-03-09Option for messing with inference of irrelevant constraintsGaëtan Gilbert
2018-03-09Cumulativity: improve treatment of irrelevant universes.Gaëtan Gilbert
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-03-09Adding a missing unification in typing.ml.Hugo Herbelin
2018-03-09Merge PR #6895: [compat] Remove "Refolding Reduction" option.Maxime Dénès
2018-03-09Merge PR #6747: Relax conversion of constructors according to the pCuIC modelMaxime Dénès
2018-03-08Merge PR #6893: Cleanup UState API usageMaxime Dénès
2018-03-08[compat] Remove "Refolding Reduction" option.Emilio Jesus Gallego Arias
2018-03-08Leave cumul constructor universes as is during unifMatthieu Sozeau
2018-03-08Relax conversion of constructors according to the pCuIC modelMatthieu Sozeau
2018-03-07Merge PR #6905: Fix make ml-docMaxime Dénès
2018-03-07Merge PR #6790: Allow universe declarations for [with Definition].Maxime Dénès
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-03-06Merge PR #6900: [compat] Remove "Tactic Pattern Unification"Maxime Dénès
2018-03-05Replace invalid tag @raises in ocamldoc comments with @raisemrmr1993
2018-03-05Allow universe declarations for [with Definition].Gaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-05Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-09 15:54:23 +0000