aboutsummaryrefslogtreecommitdiff
path: root/tuto1/src/simple_declare.ml
AgeCommit message (Expand)Author
2018-11-02Fix for coq/coq#8515 (command driven attributes)Gaƫtan Gilbert
2018-10-31Revert "Merge pull request #13 from herbelin/master+adapt-coq8718-declaration...Yves Bertot
2018-10-30Adapting to Coq PR #8718: declare_definition now takes a UState.t.Hugo Herbelin
2018-10-11[coq] Adapt for PR #8704.Emilio Jesus Gallego Arias
2018-10-01adapts to master on Oct. 1st 2018, but warnings remainYves Bertot
2018-05-04follows G. Gilbert's suggestion to have polymorphism following a flagYves Bertot
2018-05-04A modified version that includes code proposed by G. GilbertYves Bertot
2018-05-03little cleanup on the defining command, and question in commentsYves Bertot
2018-05-03This version contains a simple command that defines a new constantYves Bertot