aboutsummaryrefslogtreecommitdiff
path: root/vernac/auto_ind_decl.ml
AgeCommit message (Expand)Author
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-07-13Remove the function Global.type_of_global_unsafe.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
2017-05-27[coqlib] Move `Coqlib` to `library/`.Emilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-02Merge PR#582: Fix warningsMaxime Dénès
2017-05-01More consistent writing of de Bruijn.Théo Zimmermann
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-21[pp] [ide] Minor cleanups in pp code.Emilio Jesus Gallego Arias
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias