aboutsummaryrefslogtreecommitdiff
path: root/pretyping/vnorm.ml
AgeCommit message (Expand)Author
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
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Inv API using EConstr.Pierre-Marie Pédrot
2017-02-14Vnorm API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2016-09-27Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-23Fix bug #5096: [vm_compute] is exponentially slower than [native_compute].Pierre-Marie Pédrot
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 18:31:10 +0000