| _ -> assert false
;;
+let unvariant newt =
+ 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
+;;
+
let is_a_double_coercion t =
let rec subst_nth n x l =
match n,l with
let selected =
HExtlib.list_findopt
(fun (metasenv,last,c) _ ->
- match c with
- | c when not (CoercGraph.is_composite c) ->
- debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
- None
- | c ->
let subst,metasenv,ugraph =
fo_unif_subst subst context metasenv last head ugraph in
debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
ugraph
in
debug_print (lazy (" has type: "^ pp tty));
- Some (coerc,tty,subst,metasenv,ugraph)
+
+ Some (unvariant coerc,tty,subst,metasenv,ugraph)
with
| Uncertain _ | RefineFailure _
| HExtlib.Localized (_,Uncertain _)
if b then
Some ((t,infty), subst, metasenv, ugraph)
else
+ let newt = unvariant newt in
Some ((newt,newty), subst, metasenv, ugraph)
with
| Uncertain _ -> uncertain := true; None