aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-04-10Remove calls to Global.env from EvarsolveMaxime Dénès
2019-04-10Remove calls to Global.env and Libobject from RecordopsMaxime Dénès
2019-04-10Remove calls to Global.env in TypingMaxime Dénès
2019-04-10Remove calls to Global.env in Glob_opsMaxime Dénès
2019-04-10Remove calls to Global.env in PatternopsMaxime Dénès
2019-04-10Remove call to global env in pretyping.mlMaxime Dénès
2019-04-10Functionalize env in type classesMaxime Dénès
2019-04-10Move vernac-related part of coercions to vernacMaxime Dénès
2019-04-10Remove one call to Global.env in DetypingMaxime Dénès
2019-04-10Remove calls to global env from indrecMaxime Dénès
2019-04-10Fix constant order in heads.mlMaxime Dénès
2019-04-08Don't store closures in summary (reduction effects)Gaëtan Gilbert
2019-04-08Merge PR #9915: Remove cache in HeadsEnrico Tassi
2019-04-05[native compiler] Normalize before destructuring sortMaxime Dénès
2019-04-05Remove cache in HeadsMaxime Dénès
2019-04-03Merge PR #9078: Provide a faster bound name generation algorithm through a flagVincent Laporte
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
2019-04-02Fast name generation in detyping.Pierre-Marie Pédrot
2019-04-02Abstract away the name generation algorithm in Detyping.Pierre-Marie Pédrot
2019-04-02Pass flags through a record in Detyping.Pierre-Marie Pédrot
2019-04-01Merge PR #9870: Minor refactoring in canonical structuresEnrico Tassi
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2019-03-30[Canonical structures] Minor refactoringVincent Laporte
2019-03-30[Canonical structures] Minor cleaningVincent Laporte
2019-03-28Merge PR #9129: [proof] Removal of imperative state ; interpretation layers o...Maxime Dénès
2019-03-28Merge PR #9743: Relax the ambiguous path condition of coercionEnrico Tassi
2019-03-27[geninterp] Track polymorphic status in tactic interpretation.Emilio Jesus Gallego Arias
2019-03-26[evarconv] solve_simple_eqn is weaker than miller pattern (fix #9663)Enrico Tassi
2019-03-26Declare initial hint databases in preludeMaxime Dénès
2019-03-25Remove `Automatic Coercions Import` option.Maxime Dénès
2019-03-18Fix constr_matching on SPropGaëtan Gilbert
2019-03-14Relax the ambiguous path condition of coercionKazuhiko Sakaguchi
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-14Make Sorts.t privateGaëtan Gilbert
2019-03-12Merge PR #9632: Fix #9631: Instance: anomaly grounding non evar-free termEmilio Jesus Gallego Arias
2019-03-12Merge PR #7819: Ho matching occ selEnrico Tassi
2019-03-06Merge PR #9476: Constructor type information uses the expanded form.Gaëtan Gilbert
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
2019-02-28Print location for type error in pattern variableGaëtan Gilbert
2019-02-25Fix #9631: Instance: anomaly grounding non evar-free termGaëtan Gilbert
2019-02-19Merge PR #9297: Two fixes in printing notations with patternsEmilio Jesus Gallego Arias
2019-02-19Notations: Enforce strong evaluation of cases_pattern_of_glob_constr.Hugo Herbelin
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-02-08evarsolve transp_state and comments fixesMatthieu Sozeau
2019-02-08evarconf transp state and comments fixesMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:08:57 +0000