[location] [ast] Port module AST to CAst

5 files changed, 13 insertions, 13 deletions

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index dc43930e4..9d50b6e6f 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -631,14 +631,14 @@ let subst_var_with_hole occ tid t =
   let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in
   let locref = ref 0 in
   let rec substrec = function
-    | (_, GVar id) as x -> 
+    | { CAst.v = GVar id } as x -> 
         if Id.equal id tid 
         then
 	  (decr occref;
 	   if Int.equal !occref 0 then x
            else
 	     (incr locref;
-              Loc.tag ~loc:(Loc.make_loc (!locref,0)) @@
+              CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
 	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),
                      Misctypes.IntroAnonymous, None)))
         else x
@@ -651,12 +651,12 @@ let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
   let rec substrec = function
-    | _, GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) ->
+    | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) } ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
 	  (incr locref;
-           Loc.tag ~loc:(Loc.make_loc (!locref,0)) @@
+           CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
 	   GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s))
     | c -> map_glob_constr_left_to_right substrec c
   in
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 1f40c67b5..b4a0e46ae 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -123,7 +123,7 @@ TACTIC EXTEND rewrite_strat
 END
 
 let clsubstitute o c =
-  let is_tac id = match fst (fst (snd c)) with (_, GVar id') when Id.equal id' id -> true | _ -> false in
+  let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id'} when Id.equal id' id -> true | _ -> false in
     Tacticals.onAllHypsAndConcl
       (fun cl ->
         match cl with
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 58473d7dd..87b79374e 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1085,7 +1085,7 @@ type 'a extra_genarg_printer =
   let strip_prod_binders_glob_constr n (ty,_) =
     let rec strip_ty acc n ty =
       if Int.equal n 0 then (List.rev acc, (ty,None)) else
-        match Loc.obj ty with
+        match ty.CAst.v with
             Glob_term.GProd(na,Explicit,a,b) ->
               strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b
           | _ -> error "Cannot translate fix tactic: not enough products" in
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 566dd8ed7..8751a14c7 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -108,12 +108,12 @@ let intern_ltac_variable ist = function
 
 let intern_constr_reference strict ist = function
   | Ident (_,id) as r when not strict && find_hyp id ist ->
-      (Loc.tag @@ GVar id), Some (CAst.make @@ CRef (r,None))
+      (CAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None))
   | Ident (_,id) as r when find_var id ist ->
-      (Loc.tag @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None))
+      (CAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None))
   | r ->
       let loc,_ as lqid = qualid_of_reference r in
-      Loc.tag @@ GRef (locate_global_with_alias lqid,None), 
+      CAst.make @@ GRef (locate_global_with_alias lqid,None), 
 	if strict then None else Some (CAst.make @@ CRef (r,None))
 
 let intern_move_location ist = function
@@ -272,7 +272,7 @@ let intern_destruction_arg ist = function
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
 	match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with
-	| (loc, GVar id), _ -> clear,ElimOnIdent (loc,id)
+	| {loc; CAst.v = GVar id}, _ -> clear,ElimOnIdent (loc,id)
 	| c -> clear,ElimOnConstr (c,NoBindings)
       else
 	clear,ElimOnIdent (loc,id)
@@ -350,7 +350,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
       | _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in
       let sign = { Constrintern.ltac_vars = ist.ltacvars; Constrintern.ltac_bound = Id.Set.empty } in
       let c = Constrintern.interp_reference sign r in
-      match Loc.obj c with
+      match c.CAst.v with
       | GRef (r,None) ->
           Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
       | GVar id ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 449027b52..91bc46fe7 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -697,7 +697,7 @@ let interp_typed_pattern ist env sigma (_,c,_) =
 let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
   let try_expand_ltac_var sigma x =
     try match dest_fun x with
-    | (_, GVar id), _ ->
+    | { CAst.v = GVar id }, _ ->
       let v = Id.Map.find id ist.lfun in
       sigma, List.map inj_fun (coerce_to_constr_list env v)
     | _ ->
@@ -1072,7 +1072,7 @@ let interp_destruction_arg ist gl arg =
 	if Tactics.is_quantified_hypothesis id gl then
           keep,ElimOnIdent (loc,id)
 	else
-          let c = (Loc.tag ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
+          let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
           let f = { delayed = fun env sigma ->
             let sigma = Sigma.to_evar_map sigma in
             let (sigma,c) = interp_open_constr ist env sigma c in