]> matita.cs.unibo.it Git - helm.git/commitdiff
Rel to hidden hypotheses are now printed as _hidden_n.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 4 Feb 2004 23:41:14 +0000 (23:41 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 4 Feb 2004 23:41:14 +0000 (23:41 +0000)
helm/ocaml/cic_proof_checking/cicPp.ml

index 5c5bd71fff473b8522256c633a0fa7c5e9546c74..152cdd19835f602987b34bb762987cdb481b3d09 100644 (file)
@@ -69,7 +69,7 @@ let rec pp t l =
          (match get_nth l n with
              Some (C.Name s) -> s
            | Some C.Anonymous -> "__" ^ string_of_int n
-           | _ -> raise CicPpInternalError
+           | None -> "_hidden_" ^ string_of_int n
          )
         with
          NotEnoughElements -> string_of_int (List.length l - n)