aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-23[api] Move `Vernacexpr` to parsing.Emilio Jesus Gallego Arias
2018-05-23[api] Move `opacity_flag` to `Proof_global`.Emilio Jesus Gallego Arias
2018-05-22Merge PR #7384: Split UniversesPierre-Marie Pédrot
2018-05-18Merge PR #6965: [api] Move universe syntax to `Glob_term`Pierre-Marie Pédrot
2018-05-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
2018-05-17Stop using Universes.subst(_opt)_univs_constrGaëtan Gilbert
2018-05-17Make set minimization option internal to UniversesGaëtan Gilbert
2018-05-17Merge PR #7359: Reduce usage of evar_map referencesPierre-Marie Pédrot
2018-05-15Merge PR #7213: Do not compute constr matching context if not used.Matthieu Sozeau
2018-05-14Use evd_combX in Cases.Gaëtan Gilbert
2018-05-14Typing implementation doesn't use evdref.Gaëtan Gilbert
2018-05-14Deprecate Typing.e_* functionsGaëtan Gilbert
2018-05-14Typing: define functional alternatives to e_* functionsGaëtan Gilbert
2018-05-11set_solve_evars doesn't use an evar_map refGaëtan Gilbert
2018-05-11Deprecate Evarconv.e_conv,e_cumulGaëtan Gilbert
2018-05-11Deprecate most evarutil evdref functionsGaëtan Gilbert
2018-05-08[api] Move universe syntax to `Glob_term`Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-05-04Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.Pierre-Marie Pédrot
2018-05-01[api] Move bullets and goals selectors to `proofs/`Emilio Jesus Gallego Arias
2018-04-29Strict focusing using Default Goal Selector.Gaëtan Gilbert
2018-04-27Merge PR #7358: Fix #7356: missing lift when interpreting default instances o...Enrico Tassi
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 04:32:11 +0000