X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Frecomm%2FrecommOutput.ml;h=e93935e4aae510784a54a4c3082490b333bbd15b;hb=ccbaf3fd118c7c6425b3572a057ccc2941b7762e;hp=c48ba9304804a8adc1802271ee09b12eea018723;hpb=8fdf1af656038d0245eba64ff2531bbe94ce0e9e;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml
index c48ba9304..e93935e4a 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml
@@ -70,11 +70,19 @@ let rec write_fst och = function
   | _ :: tl                                  -> write_fst och tl
 
 and write_snd och tl s = function
+  | "axiom" :: n :: _
   | "definition" :: n :: _
+  | "corec" :: "definition" :: n :: _
+  | "rec" :: "definition" :: n :: _
   | "fact" :: n :: _
+  | "corec" :: "fact" :: n :: _
   | "lemma" :: n :: _
+  | "corec" :: "lemma" :: n :: _
+  | "theorem" :: n :: _
+  | "corec" :: "theorem" :: n :: _
   | "inductive" :: n :: _
-  | "theorem" :: n :: _     ->
+  | "coinductive" :: n :: _
+  | "|" :: n :: _                     ->
     let ss = EL.split_on_char ' ' s in
     List.iter (write_subst och n) (List.tl ss);
     write_fst och tl