Commit b9be34ab authored by MARCHE Claude's avatar MARCHE Claude

fix for bug 13849

parent 598ae8bc
......@@ -26,7 +26,7 @@ Inductive b :=
(* DO NOT EDIT BELOW *)
Theorem x1 : ((X(T, A0):(x a b)) = (X(T, A1):(x a b))).
Theorem x1 : ((X T A0:(x a b)) = (X T A1:(x a b))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
......
......@@ -271,8 +271,8 @@ and print_tnode opl opr info fmt t = match t.t_node with
if tl = [] then fprintf fmt "%a" (print_ls_real info) fs
else fprintf fmt "(%a %a)" (print_ls_real info) fs
(print_space_list (print_term info)) tl
else fprintf fmt (protect_on opl "(%a%a:%a)") (print_ls_real info) fs
(print_paren_r (print_term info)) tl (print_ty info) (t_type t)
else fprintf fmt (protect_on opl "(%a %a:%a)") (print_ls_real info) fs
(print_space_list (print_term info)) tl (print_ty info) (t_type t)
end
| Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment