aboutsummaryrefslogtreecommitdiff
path: root/pretyping/vnorm.ml
AgeCommit message (Expand)Author
2021-02-24Use Reductionops.clos_whd_flags in vm_compute and native_compute.Guillaume Melquiond
2021-02-23Normalize evars during bytecode compilation (fix #13841).Guillaume Melquiond
2021-01-04Remove redundant univ and parameter info from CaseInvertGaëtan Gilbert
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-10-11Fix #13169: vm_compute has existential crisis.Pierre-Marie Pédrot
2020-08-18Rename VM-related kernel/cfoo files to kernel/vmfooGaëtan Gilbert
2020-07-22Remove redundant data from VM case switch.Pierre-Marie Pédrot
2020-07-11Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/nativePierre-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-01UIP in SPropGaëtan Gilbert
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
2020-03-28Remove a useless reversed variant in Vars.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-14Use thunks to univ instead of lazy constr for template typingGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-01Add primitive floats to 'vm_compute'Guillaume Bertholon
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-04-29Fix #9344, #9348: incorrect unsafe to_constr in vnormGaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
2019-02-04Primitive integersMaxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-09-19Merge PR #8447: Cleaning in the retroknowledgePierre-Marie Pédrot
2018-09-17OCaml now exports the min and max non-constant tags, let's use itMaxime Dénès
2018-09-17[VM] Move structured_constant to VmvaluesMaxime Dénès
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-07-24Fix #8119: anomalies in vm_compute with let and evars.Pierre-Marie Pédrot
2018-07-05Turn a dead branch into an assertion failure in VM reification.Pierre-Marie Pédrot
2018-07-03Merge PR #7607: Simplify reification of predicate in bytecode and native comp...Pierre-Marie Pédrot
2018-06-28Deprecate Environ.retroknowledge function in favor of the projectionGaëtan Gilbert
2018-06-28Simplify reification of predicate in bytecode and native compilersMaxime Dénès
2018-06-04Preserving "canonical" form of return predicate in vm_compute.Hugo Herbelin
2018-05-28Unify pre_env and envMaxime Dénès
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04Merge PR #935: Handling evars in the VMMaxime Dénès
2018-03-03Handling evars in the VM.Pierre-Marie Pédrot
2018-03-02[VM] Unify Const_sorts and Const_type, and remove Vsort.Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-12Merge PR #1082: Fixing Print for inductive types with let-in in parametersMaxime Dénès
2018-01-26Safer VM interfacesMaxime Dénès
2017-12-14Vm_compute: taking into account let-ins in parameters of constructors.Hugo Herbelin
2017-12-02[kernel] Patch allowing to disable VM reduction.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-07-11Safe API for accessing universe constraints of global references.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Using UInfoInd for universes in inductive typesAmin Timany
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:51:37 +0000