]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/content2presMatcher.ml
metavariable context has a separator now
[helm.git] / helm / software / components / content_pres / content2presMatcher.ml
index bcb4257bfda353f4f0ba7fe010d3590da5ca674b..3c6a61a6fb169958176aef607d6a359ffd879753 100644 (file)
@@ -73,7 +73,7 @@ struct
     let add_magic m =
       let name = Util.fresh_name () in
       magic_map := (name, m) :: !magic_map;
-      Ast.Variable (Ast.TermVar (name,None))
+      Ast.Variable (Ast.TermVar (name,Ast.Level 0))
     in
     let rec aux = function
       | Ast.AttributedTerm (_, t) -> assert false
@@ -91,7 +91,7 @@ struct
       List.map2
         (fun p t ->
           match p, t with
-          | Ast.Variable (Ast.TermVar (name,l)), _ ->
+          | Ast.Variable (Ast.TermVar (name,(Ast.Self l|Ast.Level l))), _ ->
               name, (Env.TermType l, Env.TermValue t)
           | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
               name, (Env.NumType, Env.NumValue s)