]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/content2cic.ml
Reindenting.
[helm.git] / helm / ocaml / cic_omdoc / content2cic.ml
index 49468eafbefad7e1ae9484f5f0e502f6fd308ee7..7641ad90e59f9912fad9e098058cbd9ef3817201 100644 (file)
@@ -39,9 +39,9 @@ let proof2cic term2cic p =
     let module C = Cic in 
     let module Con = Content in
       let rec extend_premise_env current_env = 
-       function
+        function
             [] -> current_env
-         | p::atl ->
+          | p::atl ->
               extend_premise_env 
               ((p.Con.proof_id,(proof2cic current_env p))::current_env) atl in
       let new_premise_env = extend_premise_env premise_env p.Con.proof_apply_context in