Merge pull request coq-community#4 from erikmd/update-readme

Update the Readme (Add doc for "qualified" & Improve details)

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.