MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

Commit 284a2ad0 authored by Stefan Berghofer's avatar Stefan Berghofer
Browse files

Only expand case distinctions over free variables

parent a908f0e3
......@@ -315,8 +315,9 @@ fun expand_cases ctxt t =
fun strip_case used t =
if null (loose_bnos t)
then (apsnd (map (rename_case used)))
(Case_Translation.strip_case ctxt false t)
then (case Case_Translation.strip_case ctxt false t of
SOME (u as Free _, ps) => SOME (u, map (rename_case used) ps)
| _ => NONE)
else NONE;
fun mk_ctxt f = (fn (x, ps) => (x, map (apsnd f) ps));
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