generalize no more required before elim

[helm.git] / helm / software / components / acic_content / cicNotationPp.ml

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 2873912c0129d51b9b17e9a6f2f3aae80c144797..6ea839ce322afff694ad1af077b2253a31730aba 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -115,9 +115,12 @@ let rec pp_term ?(pp_parens = true) t =
          (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) ->
-        sprintf "let %s \\def %s in %s" (pp_capture_variable pp_term var) (pp_term ~pp_parens:true t1)
-          (pp_term ~pp_parens:true t2)
+    | Ast.LetIn ((var,t2), t1, t3) ->
+(*       let t2 = match t2 with None -> Ast.Implicit | Some t -> t in *)
+        sprintf "let %s \\def %s in %s" (pp_term var)
+(*           (pp_term ~pp_parens:true t2) *)
+          (pp_term ~pp_parens:true t1)
+          (pp_term ~pp_parens:true t3)
     | Ast.LetRec (kind, definitions, term) ->
        let rec get_guard i = function
           | []                   -> (*assert false*) Ast.Implicit
@@ -155,7 +158,7 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Sort `Set -> "Set"
     | Ast.Sort `Prop -> "Prop"
     | Ast.Sort (`Type _) -> "Type"
-    | Ast.Sort `CProp -> "CProp"
+    | Ast.Sort (`CProp _)-> "CProp"
     | Ast.Symbol (name, _) -> "'" ^ name
 
     | Ast.UserInput -> ""
@@ -176,20 +179,24 @@ let rec pp_term ?(pp_parens = true) t =
 and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term)
 and pp_substs substs = String.concat "; " (List.map pp_subst substs)
 
-and pp_pattern ((head, href, vars), term) =
-  let head_pp =
-    head ^
-    (match debug_printing, href with
-    | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
-    | _ -> "")
-  in
-  sprintf "%s \\Rightarrow %s"
-    (match vars with
-    | [] -> head_pp
-    | _ ->
-        sprintf "(%s %s)" head_pp
-          (String.concat " " (List.map (pp_capture_variable pp_term) vars)))
-    (pp_term term)
+and pp_pattern =
+ function
+    Ast.Pattern (head, href, vars), term ->
+     let head_pp =
+       head ^
+       (match debug_printing, href with
+       | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+       | _ -> "")
+     in
+     sprintf "%s \\Rightarrow %s"
+       (match vars with
+       | [] -> head_pp
+       | _ ->
+           sprintf "(%s %s)" head_pp
+             (String.concat " " (List.map (pp_capture_variable pp_term) vars)))
+       (pp_term term)
+  | Ast.Wildcard, term ->
+     sprintf "_ \\Rightarrow %s" (pp_term term)
 
 and pp_patterns patterns =
   sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns))