]> matita.cs.unibo.it Git - helm.git/commitdiff
the in clause of the match costruction was wrongly output
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 4 Sep 2006 13:43:17 +0000 (13:43 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 4 Sep 2006 13:43:17 +0000 (13:43 +0000)
components/acic_content/cicNotationPp.ml

index ff0a09265c0d6b985d4c439b70931f74f0b8eb0a..cdc0946e6f96bd2d992984bd1043ffc3a7aa9932 100644 (file)
@@ -99,7 +99,6 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Case (term, indtype, typ, patterns) ->
         sprintf "match %s%s%s with %s"
           (pp_term term)
-         (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))          
           (match indtype with
           | None -> ""
           | Some (ty, href_opt) ->
@@ -107,7 +106,8 @@ let rec pp_term ?(pp_parens = true) t =
               (match debug_printing, href_opt with
               | true, Some uri ->
                   sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
-              | _ -> ""))
+              | _ -> ""))        
+         (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))          
           (pp_patterns patterns)
     | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2)
     | Ast.LetIn (var, t1, t2) ->