aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 20:07:45 +0000