aboutsummaryrefslogtreecommitdiff
path: root/pretyping/detyping.ml
AgeCommit message (Expand)Author
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-05-05Merge PR#544: Anonymous universesMaxime Dénès
2017-05-03Allow flexible anonymous universes in instances and sorts.Gaetan Gilbert
2017-05-02applied the patch for printing types of let bindings by @herbelinAbhishek Anand (@brixpro-home)
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-24[location] Switch glob_constr to Loc.locatedEmilio Jesus Gallego Arias
2017-04-24[location] Move Glob_term.predicate_pattern to located.Emilio Jesus Gallego Arias
2017-04-24[location] Move Glob_term.cases_pattern to located.Emilio Jesus Gallego Arias
2017-04-11Merge PR#379: Introducing evar-insensitive constrsMaxime Dénès
2017-04-07Turning the printing primitive projection parameter flag off by default.Hugo Herbelin
2017-04-07Turning the printing primitive projection compatibility flag off by default.Hugo Herbelin
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-04-01Actually exporting delayed universes in the EConstr implementation.Pierre-Marie Pédrot
2017-03-24Replacing "cast surgery" in LetIn by a proper field (see PR #404).Hugo Herbelin
2017-02-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
2017-02-14Moving printing code from Evd to Termops.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers in RetypingPierre-Marie Pédrot
2017-02-14Removing some return type compatibility layers in Termops.Pierre-Marie Pédrot
2017-02-14Eliminating parts of the right-hand side compatibility layerPierre-Marie Pédrot
2017-02-14Tactic_matching API using EConstr.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Cleaning up opening of the EConstr module in pretyping folder.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:19:44 +0000