* added embedding test (HTML)

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 431449e43886c6614f5e6c8b4c417e90e75fefe4..04b769b5c2b68366d2c1f765a39d21f7b7f43f62 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1665,7 +1665,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
    | (hete, hety)::tl ->
     (match (CicReduction.whd context hetype) with
         Cic.Prod (n,s,t) ->
-         if CicReduction.are_convertible context s hety then
+         if CicReduction.are_convertible context hety s then
           (CicReduction.fdebug := -1 ;
            eat_prods context (CicSubstitution.subst hete t) tl
           )