]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/grafiteEngine.ml
in the new kernel you can type Type[i] to mean Type_i, and Type is interpreted as
[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml
index ccd02981f2f4f5a5516eb861dbca2e1cae29ca99..037a36f38ca164790ba9b5af23f75c88c752d841 100644 (file)
@@ -789,6 +789,9 @@ prerr_endline "CSC: here we should fix the height!!!";
      status, `Old [] (*CSC: TO BE FIXED *)
   | GrafiteAst.Set (loc, name, value) -> status, `Old []
 (*       GrafiteTypes.set_option status name value,[] *)
+  | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) ->
+      NCicEnvironment.add_constraint strict [false,u1] [false,u2];
+      status, `New [u1;u2]
   | GrafiteAst.NObj (loc,obj) ->
      let lexicon_status =
        match status.GrafiteTypes.ng_status with