]> matita.cs.unibo.it Git - helm.git/commitdiff
notation now digests Cic.Cast, not sure the precedence level is handled correctly
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 27 Nov 2008 10:21:52 +0000 (10:21 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 27 Nov 2008 10:21:52 +0000 (10:21 +0000)
helm/software/components/content_pres/cicNotationPres.ml
helm/software/components/content_pres/termContentPres.ml

index e6cbbf692be37411ab8c1ee8c1f10e465179cae6..77dc2b08cf8c52ebfcf2fb7f49b8e98f2eaa6903 100644 (file)
@@ -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
index 378708bce764e9e0e8010ff5b64e696f9e52f7eb..e15442970a0ac3a139d54cf2cf0b1d85d2c1ee95 100644 (file)
@@ -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)