Commit 15dac784 authored by Claude Marche's avatar Claude Marche
Browse files

Fixed missing "intro a_WT" in Coq output

parent fc14a67a
...@@ -571,7 +571,7 @@ let intros_params fmt params = ...@@ -571,7 +571,7 @@ let intros_params fmt params =
Stv.iter Stv.iter
(fun tv -> (fun tv ->
let n = id_unique iprinter tv.tv_name in let n = id_unique iprinter tv.tv_name in
fprintf fmt "@ %s" n) fprintf fmt "@ %s %s_WT" n n)
params params
let intros fmt params fmla = let intros fmt params fmla =
......
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