diff --git a/TODO b/TODO index 35354137249759e7686c55bbafa20bb40e305733..e0fdf9de3bb44ea229d56e31186cee8f2b5a04b9 100644 --- a/TODO +++ b/TODO @@ -32,8 +32,6 @@ library/gallery migration - no warning on lemma functions cf examples/tests/lemma_functions.mlw - - cloning a recursive data type (e.g. clone list.List) - - "old" and "at" in program code gives a syntax error (bench/programs/bad-to-keep/old3.mlw), we can do better diff --git a/src/mlw/pmodule.ml b/src/mlw/pmodule.ml index 621242afe08cad03699d5381bd4edc5557a8a1d9..ae8b73dabca0221a3d7f95200e7928334585aff2 100644 --- a/src/mlw/pmodule.ml +++ b/src/mlw/pmodule.ml @@ -639,8 +639,8 @@ let clone_type_decl inst cl tdl = if Sits.mem s alg then begin if not (Mts.mem s.its_ts cl.ts_table) then let id = id_clone s.its_ts.ts_name in - let s = create_rec_itysymbol id s.its_ts.ts_args in - cl.ts_table <- Mts.add s.its_ts s cl.ts_table + let s' = create_rec_itysymbol id s.its_ts.ts_args in + cl.ts_table <- Mts.add s.its_ts s' cl.ts_table end else Opt.iter (visit alg s) (Mits.find_opt s def); List.iter down tl | Ityvar _ -> () in