parameter sintax added to axiom statement

[helm.git] / helm / software / components / content_pres / content2presMatcher.ml

diff --git a/helm/software/components/content_pres/content2presMatcher.ml b/helm/software/components/content_pres/content2presMatcher.ml
index 7e080ea6956a901180b40f719be98753af00267a..23f62092496d16eb7b47dd086d0ba0b017671616 100644 (file)
--- a/helm/software/components/content_pres/content2presMatcher.ml
+++ b/helm/software/components/content_pres/content2presMatcher.ml
@@ -36,9 +36,14 @@ let get_tag term0 =
   let subterms = ref [] in
   let map_term t =
     subterms := t :: !subterms ; 
-    Ast.Implicit
+    Ast.Implicit `JustOne
   in
-  let rec aux t = CicNotationUtil.visit_ast ~special_k map_term t
+  let rec aux t = 
+    CicNotationUtil.visit_ast 
+      ~map_xref_option:(fun _ -> None)
+      ~map_case_indty:(fun _ -> None)
+      ~map_case_outtype:(fun _ _ -> None)
+      ~special_k map_term t
   and special_k = function
     | Ast.AttributedTerm (_, t) -> aux t
     | _ -> assert false
@@ -73,7 +78,7 @@ struct
     let add_magic m =
       let name = Util.fresh_name () in
       magic_map := (name, m) :: !magic_map;
-      Ast.Variable (Ast.TermVar name)
+      Ast.Variable (Ast.TermVar (name,Ast.Level 0))
     in
     let rec aux = function
       | Ast.AttributedTerm (_, t) -> assert false
@@ -91,8 +96,8 @@ struct
       List.map2
         (fun p t ->
           match p, t with
-            Ast.Variable (Ast.TermVar name), _ ->
-              name, (Env.TermType, Env.TermValue t)
+          | 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)
           | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->