From 404cfbb5d450f3d738637cfee71aac877a4a8b1d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 27 Nov 2008 10:21:52 +0000 Subject: [PATCH] notation now digests Cic.Cast, not sure the precedence level is handled correctly --- helm/software/components/content_pres/cicNotationPres.ml | 2 +- helm/software/components/content_pres/termContentPres.ml | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml index e6cbbf692..77dc2b08c 100644 --- 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 378708bce..e15442970 100644 --- 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) -- 2.39.2