Added universes handling. The PRE_UNIVERSES tag may help ;)

[helm.git] / helm / ocaml / cic_proof_checking / cicReductionNaif.mli

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.mli b/helm/ocaml/cic_proof_checking/cicReductionNaif.mli
index 7a6255003e5368edfff2b98dabc2e8fad078da93..624eebf5d628d737adebc408447c9117f1593d86 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.mli
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.mli
@@ -30,4 +30,6 @@ exception ReferenceToCurrentProof
 exception ReferenceToInductiveDefinition
 val fdebug : int ref
 val whd : Cic.context -> Cic.term -> Cic.term
-val are_convertible : Cic.context -> Cic.term -> Cic.term -> bool
+val are_convertible :
+       Cic.context -> Cic.term -> Cic.term -> 
+       CicUniv.universe_graph -> bool * CicUniv.universe_graph