]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic_unification/cicUnification.mli
parameter sintax added to axiom statement
[helm.git] / helm / software / components / cic_unification / cicUnification.mli
index 5d0b34e28c1c3c8da76d11e2978ef5304ac19dd5..e1a6c2899e446026f352c91b33ad4e6c53f13f73 100644 (file)
@@ -56,4 +56,3 @@ val fo_unif_subst :
     Cic.term -> Cic.term -> CicUniv.universe_graph ->
       Cic.substitution * Cic.metasenv * CicUniv.universe_graph
 
-    val unif_ty : bool ref