- let newt = (* unfold coercion if `Variant *)
- match newt with
- | Cic.Appl (hd::args) ->
- let uri = CicUtil.uri_of_term hd in
- (match
- CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
- with
- | Cic.Constant (_,Some t,_,[],attrs),_
- when List.exists ((=) (`Flavour `Variant)) attrs ->
- Cic.Appl (t::args)
- | _ -> newt)
- | _ -> newt
- in