Frequently Asked Questions About Coq

Many questions are answered in the official Coq FAQ that is maintained by the Coq team.

Should I put my type in Prop_or_Set?
How does the MatchAsInReturn syntax work?
Why can't I prove (forall x, f x = g x) -> f = g? (see extensional_equality)
Isn't IntensionalEquality useless?
How do I get DependentInversion to work in my case?
Why not WTypeInsteadOfInductiveTypes?
Do False, eq, and Acc have a special status?
What is the logical strength of Coq? Can it prove the consistency of ZF or ZFC?
Do objects living in Prop ever need to be evaluated? See PropsGuardingIotaReduction.
When using eapply, how can I instantiate the question marks i.e. the ExistentialVariablesInEapply?
What is the difference between Require_Import_and_Require_Export?
How can I get Coq to always print universes?
How to define a Haskell-like notation for list comprehension?

Coqide