diff options
| -rw-r--r-- | doc/newfaq/main.tex | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex index 9b679c8284..56a8078663 100644 --- a/doc/newfaq/main.tex +++ b/doc/newfaq/main.tex @@ -699,11 +699,27 @@ that is still unknown. \Question[coqhtml]{How can I generate some HTML from my development ?} +\Question[depgraph]{How can I generate some dependancy graph from my development ?} + \Question[coqtex]{How can I cite some \Coq in my latex document ?} \Question[coqidedescr]{What is \CoqIde ?} +\Question[irrelevance]{What is proof-irrelevance ?} + + + +\Question[extraction]{What is program extraction ?} + +Program extraction consist in generating a prgram from a constructive proof. + +\Question[extraclang]{Which language can I extract to ?} + +You can extract your programs to Objective Caml and Haskell. + +\Question[extraaxiom]{How can I change extract an incomplete proof ?} +You can provide programs for your axioms. \Question[reflection]{What is a proof by reflection ?} |