Serious bug fixed: the max of two universes was computed using the polymorphic

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

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.mli b/helm/software/components/ng_kernel/nCicSubstitution.mli
index 7e3301fa8ec037135215662c955bfe58f68978d8..9b277078d4b892729325084dc335819cc6a2f836 100644 (file)
--- a/helm/software/components/ng_kernel/nCicSubstitution.mli
+++ b/helm/software/components/ng_kernel/nCicSubstitution.mli
@@ -35,7 +35,7 @@ val subst : ?avoid_beta_redexes:bool -> NCic.term -> NCic.term -> NCic.term
  *    the function is ReductionStrategy.from_env_for_unwind when psubst is
  *    used to implement nCicReduction.unwind'                              *)
 val psubst : 
-  ?avoid_beta_redexes:bool -> bool -> int -> 
+  ?avoid_beta_redexes:bool ->  
   ('a -> NCic.term) -> 'a list -> NCic.term -> 
     NCic.term