positivity check fixed

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

diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli
index 5943c926053758ea35dd95bbebd933eea6a54b44..ebbba2543fc7598c54f4016f07640a54d2861f52 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.mli
+++ b/helm/software/components/ng_kernel/nCicReduction.mli
@@ -19,7 +19,7 @@ val whd :
 val are_convertible :
   ?subst:NCic.substitution ->
   (subst:NCic.substitution ->
-   NCic.context -> NCic.term -> bool list) ->
+   NCic.context -> NCic.term -> NCic.term list -> bool list) ->
   NCic.context -> NCic.term -> NCic.term -> bool