Hi Jonathan,
A comment on "old" code:
+let lctx_olookup (ctx : lexp_context) (var : string) : (int * env_elem) option =
This function is wrong: you can't reliably lookup a lexp_context with a string. The var names available in there are only meant for debugging/prettyprinting purposes.
If you want to lookup a string in the context, you need to use the elab_context, and you can use the `senv_lookup` for that (e.g. as I do in check_case for that same purpose of seeing of an identifier refers to a constructor).
+let is_constructor loc depth args_val = match args_val with
- | [Vstring name; Velabctx ectx] -> Vcommand (fun () ->
`isconstructor` (same as `isbound`) is a pure function, so there's no need to put it in a monad.
| Some (Cons _) -> (Vint 1)| _ -> (Vint 0) )
You can use o2v_bool to conveniently return a Bool, which is a more convenient/natural return type than Int here.
Stefan