assert (CicNotationEnv.well_typed ty value); (* INVARIANT *)
(* following assertion should be a conditional that makes this
* instantiation fail *)
assert (CicNotationEnv.well_typed ty value); (* INVARIANT *)
(* following assertion should be a conditional that makes this
* instantiation fail *)
(match ty, v with
| Env.ListType ty, Env.ListValue (v :: _) ->
aux ((name, (ty, v)) :: acc) tl
(match ty, v with
| Env.ListType ty, Env.ListValue (v :: _) ->
aux ((name, (ty, v)) :: acc) tl
(match ty, v with
| Env.ListType ty, Env.ListValue (_ :: vtl) ->
aux ((name, (Env.ListType ty, Env.ListValue vtl)) :: acc) tl
(match ty, v with
| Env.ListType ty, Env.ListValue (_ :: vtl) ->
aux ((name, (Env.ListType ty, Env.ListValue vtl)) :: acc) tl