snapshot, notably:

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

diff --git a/helm/matita/matitaCicMisc.ml b/helm/matita/matitaCicMisc.ml
index 523e33ea2458d86cf249251c22eded2aa5d97992..c77ded6be1d2271d3dbf0bfd7738d878f2333620 100644 (file)
--- a/helm/matita/matitaCicMisc.ml
+++ b/helm/matita/matitaCicMisc.ml
@@ -27,11 +27,11 @@
 let cicCurrentProof (uri, metasenv, bo, ty) =
   let uri = MatitaTypes.unopt_uri uri in
     (* TODO CSC: Wrong: [] is just plainly wrong *)
-  Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])
+  Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [], [])
 
   (** create a Cic.Constant from a given proof *)
 let cicConstant (uri, metasenv, bo, ty) =
   let uri = MatitaTypes.unopt_uri uri in
     (* TODO CSC: Wrong: [] is just plainly wrong *)
-  Cic.Constant (UriManager.name_of_uri uri, Some bo, ty, [])
+  Cic.Constant (UriManager.name_of_uri uri, Some bo, ty, [], [])