new universes implementation

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index b3525d3182bcec3737d02c2883cd7402d1acf730..e8ea0769de76416d369ba4d5f5b9ff63ee0ed945 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -162,8 +162,8 @@ and type_of_aux' metasenv context t =
         in
         CicSubstitution.lift_meta l ty, subst', metasenv'
      (* TASSI: CONSTRAINT *)
-    | C.Sort (C.Type t) ->
-        let t' = CicUniv.fresh() in
+    | C.Sort (C.Type t) -> 
+        let t' = CicUniv.fresh() in 
         if not (CicUniv.add_gt t' t ) then
          assert false (* t' is fresh! an error in CicUniv *)
        else
@@ -487,7 +487,7 @@ and type_of_aux' metasenv context t =
           C.Sort s2,subst,metasenv
      | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
        (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
-       let t' = CicUniv.fresh() in
+       let t' = CicUniv.fresh() in 
        if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
          assert false ; (* not possible, error in CicUniv *)
        C.Sort (C.Type t'),subst,metasenv