Commit d5dd6cc2 authored by MARCHE Claude's avatar MARCHE Claude

Attempt to fix Why3 tactic pb with float lib

parent 2246b135
......@@ -554,7 +554,7 @@ and tr_global_ts dep env r =
| _ -> raise NotFO (* GADT *)
in
List.fold_right2 add v ts.Ty.ts_args Idmap.empty
| Ind _ ->
| Ind _ | Prod _ ->
Idmap.empty
| _ ->
assert false (* ensured by Coq typing *)
......
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