coercions that are marked as variant are unfolded when inserted

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 7b472a851b0e50839e0125a150e37163280875d1..801e80d6c003428d9e1162180b4d751f786e803a 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1452,6 +1452,19 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                 if b then 
                   Some ((t,infty), subst, metasenv, ugraph)
                 else 
+                 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
                   Some ((newt,newty), subst, metasenv, ugraph)
                with 
                | Uncertain _ -> uncertain := true; None