]> matita.cs.unibo.it Git - helm.git/blobdiff - components/cic_unification/cicRefine.ml
ooops, missing )
[helm.git] / components / cic_unification / cicRefine.ml
index f6bc9a4450dfd2500e7c02d8e220be0e560f9c60..026fc9cb1b3a72432043e279af82d7747b77645c 100644 (file)
@@ -1621,7 +1621,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
               in
               let coerced = Cic.Lambda (name_t,src2, bo) in
               debug_print (lazy ("coerced: "^ CicMetaSubst.ppterm_in_context 
-                ~metasenv subst coerced context)(;
+                ~metasenv subst coerced context));
               (coerced, expty), subst, metasenv, ugraph
           | _ -> 
             coerce_atom_to_something t infty expty subst metasenv context ugraph