Dead code removed.

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index f03752d10b10ec1cdec64077546206dbcead7af8..f01ecf785ed8524f5002d6c3f6e08610a617bdbb 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -853,7 +853,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
 
   and  avoid_double_coercion subst metasenv ugraph t ty = 
     match t with
-    | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when 
+    | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when 
       CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
           let source_carr = CoercGraph.source_of c2 in
           let tgt_carr = CicMetaSubst.apply_subst subst ty in