Commit 7bd90f16 authored by POTTIER Francois's avatar POTTIER Francois

Comment on extraction settings.

parent f2651716
......@@ -2076,6 +2076,20 @@ library, which can be found in the CompCert tree~\cite{compcert}, in the
an example if one wishes to use \menhir to generate a formally verified parser
as part of some other project.
% fp: ce pourrait être bien de documenter les directives nécessaires pour
% extraire du code efficace. D'après Xavier ce morceau de extraction.v
% est pertinent:
(* Int31 *)
Extract Inductive Int31.digits => "bool" [ "false" "true" ].
Extract Inductive Int31.int31 => "int" [ "Camlcoq.Int31.constr" ] "Camlcoq.Int31.destr".
Extract Constant Int31.twice => "Camlcoq.Int31.twice".
Extract Constant Int31.twice_plus_one => "Camlcoq.Int31.twice_plus_one".
Extract Constant Int31.compare31 => "".
Extract Constant Int31.On => "0".
Extract Constant Int31.In => "1".
% ---------------------------------------------------------------------------------------------------------------------
\section{Comparison with \ocamlyacc}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment