coq export: do not fail, only warn when a command is not translated +…

… update doc (#1091)

update doc: with -o stt_coq, parameters with no type are assumed to be of type Set

doc/options.rst

@@ -110,6 +110,8 @@ For the format ``stt_coq``, several other options are available:
 
 It tells Lambdapi which symbols of the input files are used for the encoding. Example: `encoding.lp <https://github.com/Deducteam/lambdapi/blob/master/libraries/encoding.lp>`__. The first argument ``a`` of the symbols corresponding to the builtins ``"eq"``, ``"all"`` and ``"ex"`` need not be declared as implicit.
 
+In symbol declarations or definitions, parameters with no type are assumed to be of type the term associated with the builtin ``"Set"``.
+
 * ``--no-implicits`` instructs Lambdapi that the symbols of the encoding have no implicit arguments.
 
 * ``--renaming <LP_FILE>`` where ``<LP_FILE>`` contains a sequence of builtin declarations of the form

src/export/coq.ml

@@ -295,7 +295,6 @@ let is_lem x = is_opaq x || is_priv x
 
 let command oc {elt; pos} =
   begin match elt with
-  | P_inductive _ -> wrn pos "TODO"; assert false
   | P_open ps -> string oc "Import "; list path " " oc ps; string oc ".\n"
   | P_require (true, ps) ->
       string oc "Require Import "; list path " " oc ps; string oc ".\n"
@@ -311,6 +310,7 @@ let command oc {elt; pos} =
         let p_sym_arg =
           if !stt then
             let pos = None in
+            (* Parameters with no type are assumed to be of type [Set]. *)
             let _Set = {elt=P_Iden({elt=sym Set;pos},false);pos} in
             List.map (function ids, None, b -> ids, Some _Set, b | x -> x)
               p_sym_arg
@@ -338,10 +338,9 @@ let command oc {elt; pos} =
             string oc "Axiom "; ident oc p_sym_nam; string oc " : forall";
             params_list oc p_sym_arg; string oc ", "; term oc t;
             string oc ".\n"
-          | _ -> assert false
+          | _ -> wrn pos "Command not translated."
         end
-  | P_rules _ -> wrn pos "rules are not translated"
-  | _ -> if !stt then () else (wrn pos "TODO"; assert false)
+  | _ -> wrn pos "Command not translated."
   end
 
 let ast oc = Stream.iter (command oc)