parameter sintax added to axiom statement

[helm.git] / helm / software / components / ng_kernel / nCicUntrusted.mli

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli
index 01c522ba0a557eb496c70ed1433331e4a2c025f4..7ff7f9335b6c2b5561171907fae35e12811ed73a 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUntrusted.mli
+++ b/helm/software/components/ng_kernel/nCicUntrusted.mli
@@ -42,4 +42,6 @@ val apply_subst_context : fix_projections:bool ->
 val apply_subst_metasenv : NCic.substitution -> NCic.metasenv -> NCic.metasenv
 
 val count_occurrences :
-    subst:NCic.substitution -> NCic.context -> int -> NCic.term -> int
+    subst:NCic.substitution -> int -> NCic.term -> int
+(* quick, but with false negatives (since no ~subst), check for closed terms *)
+val looks_closed : NCic.term -> bool