X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.mli;h=be1069e716ef35459836f464921e77b9315fee05;hb=d5c1f34cd226898525168e470d3e2ec273699826;hp=c3ab49e0abd84dd19a79de242dffb25999928e79;hpb=185bfc8f9c9ba49308477ee6769701f3e2977115;p=helm.git diff --git a/helm/software/components/cic_unification/cicRefine.mli b/helm/software/components/cic_unification/cicRefine.mli index c3ab49e0a..be1069e71 100644 --- a/helm/software/components/cic_unification/cicRefine.mli +++ b/helm/software/components/cic_unification/cicRefine.mli @@ -46,6 +46,5 @@ val typecheck : val insert_coercions: bool ref (* initially true *) -(* given a closed term returns it with all coercions packed *) val pack_coercion_obj: Cic.obj -> Cic.obj