1. More debugging code

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

diff --git a/helm/software/components/cic_unification/cicRefine.mli b/helm/software/components/cic_unification/cicRefine.mli
index 224a7586c957dfbf91e4704917489a348158b43a..30b264455246890438191bc2a1a0a9757db652fa 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.mli
+++ b/helm/software/components/cic_unification/cicRefine.mli
@@ -46,3 +46,6 @@ val typecheck :
 
 val insert_coercions: bool ref (* initially true *)
 
+val pack_coercion_obj: Cic.obj -> Cic.obj
+
+val pack_coercion_metasenv: Cic.metasenv -> Cic.metasenv