From e9fa1f41eb856a57ad83c798ea27c34f9e070f0f Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 8 Nov 2017 19:10:00 +0100 Subject: [PATCH] Update the Readme.md (Add doc for the "qualified" option & Improve details) --- Readme.md | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/Readme.md b/Readme.md index af91f3f..8045210 100644 --- a/Readme.md +++ b/Readme.md @@ -11,8 +11,8 @@ One way to test the plugin is to follow the following steps: * Retrieve the plugin and compile it: git clone ... - git checkout (* the correct branch *) cd paramcoq + git checkout (* the correct branch *) make sudo make install @@ -28,12 +28,16 @@ Available commands ================== The default arity is 2. -The default name is automatically generated when translating a constant (otherwise you need to provide it). -- Parametricity [Recursive] *ident* [as *name*] [arity *n*]. +- Parametricity *ident* as *name* [arity *n*]. + +Declare the translation named *name* from the translation of the constant or inductive *ident*. + +- Parametricity [Recursive] *ident* [arity *n*] [qualified]. -Declare the translation named *name* from the translation of the constant or the inductive *ident*. -You can use the recursive option to recursively translate all the constant and inductives which are used by *ident*. +The default name for the translation of the constant or inductive *ident* is automatically generated (from its unqualified name). +You can use the `Recursive` option to recursively translate all the constants and inductives which are used by *ident*. +You can use the `qualified` option to use a qualified default name for the translated constants and inductives. The default name then has the form `Module_o_Submodule_o_ident` if *ident* lies in the `Module.Submodule` namespace. - Parametricity Translation *term* [as *name*] [arity *n*]. @@ -48,8 +52,8 @@ Recursively translate everything in a module. Declare *term* to be the translation of a constant. Useful to translate terms containing section variables, or axioms. -Note that all that both translating a term or module may lead to proof obligations (for some fixpoints and opaque terms if you did not import ProofIrrelevence). +Note that both translating a term or module may lead to proof obligations (for some fixpoints and opaque terms if you did not import `ProofIrrelevence`). -- [Global | Local] Parametricity Tactict := t. +- [Global | Local] Parametricity Tactic := t. -Use the tactic t to solve proof obligations generated by the Parametricity command. +Use the tactic t to solve proof obligations generated by the `Parametricity` command.