+let rec meta_pos_name = function
+ HiddenVarTag(vars) ->
+ (* totally fake, just drop the rest, only for isos *)
+ meta_pos_name (List.hd vars)
+ | MetaPosTag(MetaPos(name,constraints,_)) -> name
+ | IdentTag(i) ->
+ (match unwrap i with
+ MetaId(name,constraints,seed,pure) -> name
+ | _ -> failwith "bad metavariable")
+ | ExprTag(e) ->
+ (match unwrap e with
+ MetaExpr(name,constraints,ty,form,pure) -> name
+ | MetaExprList(name,len,pure) -> name
+ | _ -> failwith "bad metavariable")
+ | TypeCTag(t) ->
+ (match unwrap t with
+ MetaType(name,pure) -> name
+ | _ -> failwith "bad metavariable")
+ | DeclTag(d) ->
+ (match unwrap d with
+ MetaDecl(name,pure) -> name
+ | _ -> failwith "bad metavariable")
+ | InitTag(i) ->
+ (match unwrap i with
+ MetaInit(name,pure) -> name
+ | _ -> failwith "bad metavariable")
+ | StmtTag(s) ->
+ (match unwrap s with
+ MetaStmt(name,pure) -> name
+ | _ -> failwith "bad metavariable")
+ | _ -> failwith "bad metavariable"
+
+(* --------------------------------------------------------------------- *)
+