aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2016-03-18Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-15Try eta-expansion of records only on non-recursive onesMatthieu Sozeau
2016-03-14Try eta-expansion of records only on non-recursive onesMatthieu Sozeau
2016-03-10Primitive projections: protect kernel from erroneous definitions.Matthieu Sozeau
2016-03-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-09Fix strategy of Keyed UnificationMatthieu Sozeau
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-28Slightly contracting code of evarconv.ml.Hugo Herbelin
2016-02-23Fix part of bug #4533: respect declared global transparency ofMatthieu Sozeau
2016-02-19Adding location to universes generated by the pretyper.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Using monotonic types for conversion functions.Pierre-Marie Pédrot
2016-02-15Renaming functions in Typing to stick to the standard e_* scheme.Pierre-Marie Pédrot
2016-02-15Monotonizing the Evarutil module.Pierre-Marie Pédrot
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-02-03Optimizing the computation of frozen evars.Pierre-Marie Pédrot
2016-02-03Opacifying the type of evar naming structure in Evd.Pierre-Marie Pédrot
2016-02-03More compact representation for evar resolvability flag.Pierre-Marie Pédrot
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-27Fix bug #4537: Coq 8.5 is slower in typeclass resolution.Pierre-Marie Pédrot
2016-01-23Fix bug #4519: oops, global shadowed local universe level bindings.Matthieu Sozeau
2016-01-23Fix bug #4506. Using betadeltaiota_nolet might produce terms of the formMatthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-12Fixing #4256 and #4484 (changes in evar-evar resolution made that newHugo Herbelin
2016-01-12Extend last commit: keyed unification uses full conversions on the applied co...Matthieu Sozeau
2016-01-12Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Matthieu Sozeau
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-02Remove some unused functions.Guillaume Melquiond
2016-01-02Remove duplicate declarations.Guillaume Melquiond
2016-01-02Reduce dependencies of interface files.Guillaume Melquiond
2015-12-31Merge branch 'v8.5' into trunkGuillaume Melquiond
2015-12-31Do not compose List.length with List.filter.Guillaume Melquiond
2015-12-29Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-12-17(Partial) fix for bug #4453: raise an error instead of an anomaly.Matthieu Sozeau
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-17CLEANUP: in the Reductionops moduleMatej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-15Fixing unexpected length of context in a typing function, detected byHugo Herbelin
2015-12-15Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite.Hugo Herbelin
2015-12-15API: documenting context_chop and removing a duplicate.Hugo Herbelin
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-11Optimize occur_evar_upto_types, avoiding repeateadly looking into theMatthieu Sozeau
2015-12-05Unifying betazeta_applist and prod_applist into a clearer interface.Hugo Herbelin
2015-12-05Moving extended_rel_vect/extended_rel_list to the kernel.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 08:46:14 +0000