]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/termContentPres.ml
Better handling of exceptions.
[helm.git] / helm / software / components / content_pres / termContentPres.ml
index 110c78e46e43820fc4ae280e80090f9b35c40544..d68b6a8b4bfee412eab2ac206acb46aab90f55cd 100644 (file)
@@ -151,8 +151,11 @@ let pp_ast0 t k =
            space
          ]
         in
-        let mk_case_pattern (head, href, vars) =
-          hbox true false (ident_w_href href head :: List.map aux_var vars)
+        let mk_case_pattern =
+         function
+            Ast.Pattern (head, href, vars) ->
+             hbox true false (ident_w_href href head :: List.map aux_var vars)
+          | Ast.Wildcard -> builtin_symbol "_"
         in
         let patterns' =
           List.map
@@ -465,8 +468,9 @@ let fill_pos_info l1_pattern = l1_pattern
   in
   aux true l1_pattern *)
 
+let counter = ref ~-1 
+let reset () = counter := ~-1;;
 let fresh_id =
-  let counter = ref ~-1 in
   fun () ->
     incr counter;
     !counter
@@ -575,8 +579,11 @@ let instantiate_level2 env term =
   and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt)
   and aux_branch env (pattern, term) =
     (aux_pattern env pattern, aux env term)
-  and aux_pattern env (head, hrefs, vars) =
-    (head, hrefs, List.map (aux_capture_var env) vars)
+  and aux_pattern env =
+   function
+      Ast.Pattern (head, hrefs, vars) ->
+       Ast.Pattern (head, hrefs, List.map (aux_capture_var env) vars)
+    | Ast.Wildcard -> Ast.Wildcard
   and aux_definition env (params, var, term, i) =
     (List.map (aux_capture_var env) params, aux_capture_var env var, aux env term, i)
   and aux_substs env substs =
@@ -666,3 +673,5 @@ let instantiate_level2 env term =
 
 let _ = load_patterns21 []
 
+
+