Programming in the Calculus of Inductive Constructions with Coq

Question

Sometimes I want to write programs close to bare-bone CIC (Calculus of Inductive Constructions) to get a better grasp of the internal workings. I then need to customize some settings to change the default behavior of the Coq environment, such as Set Printing Implicit.

Are there more that I can do?

Answer 1

If you want no syntactic sugar at all you should do Set Printing All.

Answer 2

You can launch coq with the -noinit option, that will avoid loading the Prelude, so as long as you don't use notations, you are pretty close to the bare CIC calculus, but as of today there is not way to disable type-inference.