X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPt.ml;h=d9d92ad6fc5b905cbb9ba0600c441fc95a4d7bf3;hb=08e9d02504942642a917c0d3e4b4795e65172d89;hp=73eeb017dad00d781bbb61f9242b2eeb8f631186;hpb=4609a07e2fe4343d94832fcaf0936223f83ba71c;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml
index 73eeb017d..d9d92ad6f 100644
--- a/helm/software/components/acic_content/cicNotationPt.ml
+++ b/helm/software/components/acic_content/cicNotationPt.ml
@@ -32,7 +32,7 @@ type induction_kind = [ `Inductive | `CoInductive ]
 type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
 type fold_kind = [ `Left | `Right ]
 
-type location = Token.flocation
+type location = Stdpp.location
 let fail floc msg =
   let (x, y) = HExtlib.loc_of_floc floc in
   failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
@@ -105,7 +105,9 @@ type term =
 
 and meta_subst = term option
 and subst = string * term
-and case_pattern = string * href option * term capture_variable list
+and case_pattern =
+   Pattern of string * href option * term capture_variable list
+ | Wildcard
 
 and box_kind = H | V | HV | HOV
 and box_spec = box_kind * bool * bool (* kind, spacing, indent *)