aboutsummaryrefslogtreecommitdiff
path: root/pretyping/detyping.ml
AgeCommit message (Expand)Author
2016-08-17Two protections against failures when printing evar_map.Hugo Herbelin
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
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-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Add an option to deactivate compatibility printing of primitiveMatthieu Sozeau
2015-11-07Experimenting printing the type of the defined term of a LetIn whenHugo Herbelin
2015-10-18Using "__" rather than this unelegant arbitrary "A" for the name of variables...Hugo Herbelin
2015-10-18Using appropriate lambda decomposition function counting let-ins whenHugo Herbelin
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-09-18Do not compress match constructs when the inner match contains no branch. (Fi...Guillaume Melquiond
2015-02-21Continuing experimentation on what part of the instance of an evarHugo Herbelin
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-13Fix issue in printing due to de Bruijn bug when constructing compatibilityMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-12-04Reactivating option "Set Printing Existential Instances" for asking printing ...Hugo Herbelin
2014-11-19Printing function for [uconstr].Arnaud Spiwack
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-10-17New experimental heuristic printing strategy for evar instances: WeHugo Herbelin
2014-10-17Re-displaying evar instances in debugger.Hugo Herbelin
2014-10-15Add an option to not print primitive projection parameters, which canMatthieu Sozeau
2014-10-10Make constrMatching and detyping more robust with respect toMatthieu Sozeau
2014-10-07Avoid a warning with Meta's names in debugger.Hugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-25Fix incorrect assert false in detyping.Matthieu Sozeau
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-13Checking typability of evar instances. Using ";" to separate bindingsHugo Herbelin
2014-09-12Parsing evar instances.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
2014-08-25Fixing the essence of naming bug #3204: use same strategy for namingHugo Herbelin
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-07-01Add toplevel commands to declare global universes and constraints.Matthieu Sozeau
2014-06-10Compute the trace of a universe inconsistency only when explicitly requiredPierre-Marie Pédrot
2014-06-04Collecting in Namegen those conventional default names that are used in diffe...Hugo Herbelin
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-28Fixing #3293 (eta-expansion at "match" printing time was failingHugo Herbelin
2014-03-03Goptions do not rely anymore on generic equality.Pierre-Marie Pédrot
2014-03-01Fixing bad comparison in Detyping.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 07:22:01 +0000