;;
let rec flexible_arg context subst = function
- | NCic.Meta (i,_) | NCic.Appl (NCic.Meta (i,_) :: _)->
+ | NCic.Meta (i,_) ->
(try
let _,_,t,_ = List.assoc i subst in
flexible_arg context subst t
with Not_found -> true)
+ | NCic.Appl (NCic.Meta (i,_) :: args)->
+ (try
+ let _,_,t,_ = List.assoc i subst in
+ flexible_arg context subst
+ (NCicReduction.head_beta_reduce ~delta:max_int
+ (NCic.Appl (t :: args)))
+ with Not_found -> true)
(* this is a cheap whd, it only performs zeta-reduction.
*
* it works when the **omissis** disambiguation algorithm
menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty
| `Sort ->
let ty = NCic.Implicit (`Typeof n) in
- mk_meta (tyof attrs) n metasenv [] (`WithType ty)
+ mk_meta (`IsSort::tyof attrs) n metasenv [] (`WithType ty)
| `Type ->
let metasenv, _, ty, _ =
mk_meta (tyof attrs) (newmeta ()) metasenv context `Sort in