notation now digests Cic.Cast, not sure the precedence level is handled correctly

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index e6cbbf692be37411ab8c1ee8c1f10e465179cae6..77dc2b08cf8c52ebfcf2fb7f49b8e98f2eaa6903 100644 (file)
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/components/content_pres/cicNotationPres.ml
@@ -331,7 +331,7 @@ let render ids_to_uris ?(prec=(-1)) =
           | `Raw _ -> ()
           | `Level (-1) -> reset := true
           | `Level child_prec ->
-              assert (!expected_level = None);
+(*               assert (!expected_level = None); *)
               expected_level := !inferred_level;
               inferred_level := Some child_prec
           | `IdRef xref -> new_xref := xref :: !new_xref

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 378708bce764e9e0e8010ff5b64e696f9e52f7eb..e15442970a0ac3a139d54cf2cf0b1d85d2c1ee95 100644 (file)
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -598,6 +598,8 @@ let instantiate_level2 env term =
     | Ast.Magic magic -> aux_magic env magic
     | Ast.Variable var -> aux_variable env var
 
+    | Ast.Cast (t, ty) -> Ast.Cast (aux env t, aux env ty)
+
     | _ -> assert false
   and aux_opt env = function
     | Some term -> Some (aux env term)