diff options
author | 2018-02-14 06:57:40 +0100 | |
---|---|---|
committer | 2018-03-09 23:23:40 +0100 | |
commit | 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 (patch) | |
tree | 9ffa30a21f0d5b80aaeae66955e652f185929498 /tactics/tacticals.ml | |
parent | 5f989f48eaaf5e13568fce9849f40bc554ca0166 (diff) |
[located] More work towards using CAst.t
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
Diffstat (limited to 'tactics/tacticals.ml')
-rw-r--r-- | tactics/tacticals.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 789cc35ee..958a205a1 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -185,8 +185,8 @@ let check_or_and_pattern_size ?loc check_and names branchsigns = match names with | IntroAndPattern l -> if not (Int.equal n 1) then errn n; - let l' = List.filter (function _,IntroForthcoming _ -> true | _,IntroNaming _ | _,IntroAction _ -> false) l in - if l' != [] then errforthcoming ?loc:(fst (List.hd l')); + let l' = List.filter CAst.(function {v=IntroForthcoming _} -> true | {v=IntroNaming _} | {v=IntroAction _} -> false) l in + if l' != [] then errforthcoming ?loc:(List.hd l').CAst.loc; if check_and then let p1 = List.count (fun x -> x) branchsigns.(0) in let p2 = List.length branchsigns.(0) in @@ -194,7 +194,7 @@ let check_or_and_pattern_size ?loc check_and names branchsigns = if not (Int.equal p p1 || Int.equal p p2) then err1 p1 p2; if Int.equal p p1 then IntroAndPattern - (List.extend branchsigns.(0) (Loc.tag @@ IntroNaming IntroAnonymous) l) + (List.extend branchsigns.(0) (CAst.make @@ IntroNaming IntroAnonymous) l) else names else @@ -218,7 +218,7 @@ let get_and_check_or_and_pattern ?loc = get_and_check_or_and_pattern_gen ?loc tr let compute_induction_names_gen check_and branchletsigns = function | None -> Array.make (Array.length branchletsigns) [] - | Some (loc,names) -> + | Some {CAst.loc;v=names} -> let names = fix_empty_or_and_pattern (Array.length branchletsigns) names in get_and_check_or_and_pattern_gen check_and ?loc names branchletsigns |