dep.opt regenerated

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index a263a2eb4dc4fcece602edd7dfc1916f062ca9d6..7b26cf6db06e0666c1f92dda0e8f3bd2020bf675 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1191,7 +1191,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
       | CoercGraph.SomeCoercion candidates -> 
          let selected =
            HExtlib.list_findopt
-             (function (metasenv,last,c) ->
+             (fun (metasenv,last,c) _ ->
                match c with 
                | c when not (CoercGraph.is_composite c) -> 
                    debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
@@ -1345,7 +1345,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                 ugraph in
               match
                 HExtlib.list_findopt
-                 (fun (he,hetype,subst,metasenv,ugraph) ->
+                 (fun (he,hetype,subst,metasenv,ugraph) _ ->
                    (* {{{ *)debug_print (lazy ("Try fix: "^
                     CicMetaSubst.ppterm_in_context ~metasenv subst he context));
                    debug_print (lazy (" of type: "^
@@ -1985,7 +1985,7 @@ let typecheck metasenv uri obj ~localization_tbl =
      let ty',sort,metasenv,ugraph =
       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
      begin
-      match sort with
+       match CicReduction.whd ~delta:true [] sort with
          Cic.Sort _
        (* instead of raising Uncertain, let's hope that the meta will become
           a sort *)