aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2020-09-03Comment AllowedEvars APIMaxime Dénès
2020-09-02More efficient data structure for allowed evarsMaxime Dénès
2020-09-02Abstract type for allowed evarsMaxime Dénès
2020-09-02Replace `frozen` by `allowed` evars in evarconv, and delay themMaxime Dénès
2020-08-31Use a faster algorithm to check for class existence.Pierre-Marie Pédrot
2020-08-27Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfooPierre-Marie Pédrot
2020-08-19Merge PR #12725: Store evar identity instances in evarinfo / named_context_valEnrico Tassi
2020-08-18Rename VM-related kernel/cfoo files to kernel/vmfooGaëtan Gilbert
2020-08-17Merge PR #12751: Fixes reduction effect printing in the presence of non purel...Pierre-Marie Pédrot
2020-08-11Small code simplification in contract_(co)fix.Pierre-Marie Pédrot
2020-08-11Move reduce_mind_case from Reductionops to Tacred.Pierre-Marie Pédrot
2020-08-06Actually use the default instance stored inside named_context_val.Pierre-Marie Pédrot
2020-08-06Use the evarinfo-stored identity substitution where applicable.Pierre-Marie Pédrot
2020-07-24Fixes reduction effect printing in the presence of non purely applicative sta...Hugo Herbelin
2020-07-22Remove redundant data from VM case switch.Pierre-Marie Pédrot
2020-07-18Merge PR #12588: [exn] Remove some uses of printPierre-Marie Pédrot
2020-07-13Don't catch anomalies for evarconv "cannot find an instance" errorGaëtan Gilbert
2020-07-11Merge PR #12650: Recordops: unify struc_typ summary record and libobject entr...Pierre-Marie Pédrot
2020-07-11Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/nativePierre-Marie Pédrot
2020-07-10Merge PR #12638: Some changes of representation in TacredEnrico Tassi
2020-07-09[error handling] Anomaly in Conversion is a "precatchable_exception"Emilio Jesus Gallego Arias
2020-07-09[reductionops] Comment about absorption of anomalies.Emilio Jesus Gallego Arias
2020-07-09[exn] Remove some uses of printEmilio Jesus Gallego Arias
2020-07-09Recordops: unify struc_typ summary record and libobject entry struc_tupleGaëtan Gilbert
2020-07-08Merge PR #12627: Fix Canonical with universe polymorphism and primitive proje...Enrico Tassi
2020-07-08Remove Evarutil.new_evar_instance from the API.Pierre-Marie Pédrot
2020-07-06Correctly readback blocked CaseInvert matches in VM/nativeGaëtan Gilbert
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-05Further cleanup of dead code in the Reductionops API.Pierre-Marie Pédrot
2020-07-05Remove the last use of the Stack module in Tacred.Pierre-Marie Pédrot
2020-07-05Inline make_elim_fun in Tacred.Pierre-Marie Pédrot
2020-07-05Inline the Reductionops.fix_recarg function.Pierre-Marie Pédrot
2020-07-05Inline mutual recursion helpers in simpl implementation.Pierre-Marie Pédrot
2020-07-05Stop back-and-forth array to list conversions in simpl.Pierre-Marie Pédrot
2020-07-05Fix Canonical with universe polymorphism and primitive projectionGaëtan Gilbert
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-23Merge PR #12530: Fix glob_sort_family for SPropMaxime Dénès
2020-06-19Share the identity instance in pretyping environments.Pierre-Marie Pédrot
2020-06-19Do not reallocate named_context_val of the pretyping environment.Pierre-Marie Pédrot
2020-06-17Fix glob_sort_family for SPropGaëtan Gilbert
2020-06-04Move the Cbn module to tactics/.Pierre-Marie Pédrot
2020-06-04Further cleanup.Pierre-Marie Pédrot
2020-06-04Move the cbn reduction to its own file, and simplify the RAKAM accordingly.Pierre-Marie Pédrot
2020-05-29Fixes #12418 (inference of return clause meets assert false).Hugo Herbelin
2020-05-22Merge PR #12295: Fixes #12233: printing environment corrupted with eta-expans...Pierre-Marie Pédrot
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
2020-05-13Fixes #12233 (wrong printing env in presence of match branches eta-expansion).Hugo Herbelin
2020-05-12Do not use Unsafe.to_constr for old refiner conclusion.Pierre-Marie Pédrot
2020-05-10Further cleanup: remove the local_reduction_function type.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:51:34 +0000