ported to new getter interface

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index cb420d267ecf41f866a96dcb2695d1a95a93c00f..5919a7bfc696f0fa05f16accf153b0f55397dd84 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -132,18 +132,14 @@ let eval_coercion status coercion =
     match coercion with 
     | Cic.Const (uri,_)
     | Cic.Var (uri,_) ->
-        let o,_ = 
-          CicEnvironment.get_obj CicUniv.empty_ugraph uri 
-        in
+        let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         (match o with
         | Cic.Constant (_,_,ty,_,_)
         | Cic.Variable (_,_,ty,_,_) ->
             uri,ty
         | _ -> assert false)
     | Cic.MutConstruct (uri,t,c,_) ->
-        let o,_ = 
-          CicEnvironment.get_obj CicUniv.empty_ugraph uri 
-        in
+        let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         (match o with
         | Cic.InductiveDefinition (l,_,_,_) ->
             let (_,_,_,cl) = List.nth l t in