[coq] Adapt to coq/coq#6831.

This removes uses of `Loc.t` in favor of `CAst.t`.

1 files changed, 49 insertions, 50 deletions

diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 2f6c97f08b..05b9f4141f 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Names
 open Tac2expr
 
@@ -15,65 +14,65 @@ open Tac2expr
 
 type 'a or_anti =
 | QExpr of 'a
-| QAnti of Id.t located
+| QAnti of Id.t CAst.t
 
 type quantified_hypothesis =
-| QAnonHyp of int located
-| QNamedHyp of Id.t located
+| QAnonHyp of int CAst.t
+| QNamedHyp of Id.t CAst.t
 
 type bindings_r =
 | QImplicitBindings of Constrexpr.constr_expr list
-| QExplicitBindings of (quantified_hypothesis located or_anti * Constrexpr.constr_expr) located list
+| QExplicitBindings of (quantified_hypothesis CAst.t or_anti * Constrexpr.constr_expr) CAst.t list
 | QNoBindings
 
-type bindings = bindings_r located
+type bindings = bindings_r CAst.t
 
 type intro_pattern_r =
 | QIntroForthcoming of bool
 | QIntroNaming of intro_pattern_naming
 | QIntroAction of intro_pattern_action
 and intro_pattern_naming_r =
-| QIntroIdentifier of Id.t located or_anti
-| QIntroFresh of Id.t located or_anti
+| QIntroIdentifier of Id.t CAst.t or_anti
+| QIntroFresh of Id.t CAst.t or_anti
 | QIntroAnonymous
 and intro_pattern_action_r =
 | QIntroWildcard
 | QIntroOrAndPattern of or_and_intro_pattern
-| QIntroInjection of intro_pattern list located
+| QIntroInjection of intro_pattern list CAst.t
 (* | QIntroApplyOn of Empty.t (** Not implemented yet *) *)
 | QIntroRewrite of bool
 and or_and_intro_pattern_r =
-| QIntroOrPattern of intro_pattern list located list
-| QIntroAndPattern of intro_pattern list located
+| QIntroOrPattern of intro_pattern list CAst.t list
+| QIntroAndPattern of intro_pattern list CAst.t
 
-and intro_pattern = intro_pattern_r located
-and intro_pattern_naming = intro_pattern_naming_r located
-and intro_pattern_action = intro_pattern_action_r located
-and or_and_intro_pattern = or_and_intro_pattern_r located
+and intro_pattern = intro_pattern_r CAst.t
+and intro_pattern_naming = intro_pattern_naming_r CAst.t
+and intro_pattern_action = intro_pattern_action_r CAst.t
+and or_and_intro_pattern = or_and_intro_pattern_r CAst.t
 
 type occurrences_r =
 | QAllOccurrences
-| QAllOccurrencesBut of int located or_anti list
+| QAllOccurrencesBut of int CAst.t or_anti list
 | QNoOccurrences
-| QOnlyOccurrences of int located or_anti list
+| QOnlyOccurrences of int CAst.t or_anti list
 
-type occurrences = occurrences_r located
+type occurrences = occurrences_r CAst.t
 
-type hyp_location = (occurrences * Id.t located or_anti) * Locus.hyp_location_flag
+type hyp_location = (occurrences * Id.t CAst.t or_anti) * Locus.hyp_location_flag
 
 type clause_r =
   { q_onhyps : hyp_location list option; q_concl_occs : occurrences; }
 
-type clause = clause_r located
+type clause = clause_r CAst.t
 
-type constr_with_bindings = (Constrexpr.constr_expr * bindings) located
+type constr_with_bindings = (Constrexpr.constr_expr * bindings) CAst.t
 
 type destruction_arg_r =
 | QElimOnConstr of constr_with_bindings
-| QElimOnIdent of Id.t located
-| QElimOnAnonHyp of int located
+| QElimOnIdent of Id.t CAst.t
+| QElimOnAnonHyp of int CAst.t
 
-type destruction_arg = destruction_arg_r located
+type destruction_arg = destruction_arg_r CAst.t
 
 type induction_clause_r = {
   indcl_arg : destruction_arg;
@@ -82,33 +81,33 @@ type induction_clause_r = {
   indcl_in : clause option;
 }
 
-type induction_clause = induction_clause_r located
+type induction_clause = induction_clause_r CAst.t
 
 type conversion_r =
 | QConvert of Constrexpr.constr_expr
 | QConvertWith of Constrexpr.constr_expr * Constrexpr.constr_expr
 
-type conversion = conversion_r located
+type conversion = conversion_r CAst.t
 
 type multi_r =
-| QPrecisely of int located
-| QUpTo of int located
+| QPrecisely of int CAst.t
+| QUpTo of int CAst.t
 | QRepeatStar
 | QRepeatPlus
 
-type multi = multi_r located
+type multi = multi_r CAst.t
 
 type rewriting_r = {
-  rew_orient : bool option located;
+  rew_orient : bool option CAst.t;
   rew_repeat : multi;
   rew_equatn : constr_with_bindings;
 }
 
-type rewriting = rewriting_r located
+type rewriting = rewriting_r CAst.t
 
 type dispatch_r = raw_tacexpr option list * (raw_tacexpr option * raw_tacexpr option list) option
 
-type dispatch = dispatch_r located
+type dispatch = dispatch_r CAst.t
 
 type red_flag_r =
 | QBeta
@@ -117,52 +116,52 @@ type red_flag_r =
 | QFix
 | QCofix
 | QZeta
-| QConst of Libnames.reference or_anti list located
-| QDeltaBut of Libnames.reference or_anti list located
+| QConst of Libnames.reference or_anti list CAst.t
+| QDeltaBut of Libnames.reference or_anti list CAst.t
 
-type red_flag = red_flag_r located
+type red_flag = red_flag_r CAst.t
 
-type strategy_flag = red_flag list located
+type strategy_flag = red_flag list CAst.t
 
 type constr_match_pattern_r =
 | QConstrMatchPattern of Constrexpr.constr_expr
 | QConstrMatchContext of Id.t option * Constrexpr.constr_expr
 
-type constr_match_pattern = constr_match_pattern_r located
+type constr_match_pattern = constr_match_pattern_r CAst.t
 
-type constr_match_branch = (constr_match_pattern * raw_tacexpr) located
+type constr_match_branch = (constr_match_pattern * raw_tacexpr) CAst.t
 
-type constr_matching = constr_match_branch list located
+type constr_matching = constr_match_branch list CAst.t
 
 type goal_match_pattern_r = {
   q_goal_match_concl : constr_match_pattern;
   q_goal_match_hyps : (Misctypes.lname * constr_match_pattern) list;
 }
 
-type goal_match_pattern = goal_match_pattern_r located
+type goal_match_pattern = goal_match_pattern_r CAst.t
 
-type goal_match_branch = (goal_match_pattern * raw_tacexpr) located
+type goal_match_branch = (goal_match_pattern * raw_tacexpr) CAst.t
 
-type goal_matching = goal_match_branch list located
+type goal_matching = goal_match_branch list CAst.t
 
 type hintdb_r =
 | QHintAll
-| QHintDbs of Id.t located or_anti list
+| QHintDbs of Id.t CAst.t or_anti list
 
-type hintdb = hintdb_r located
+type hintdb = hintdb_r CAst.t
 
 type move_location_r =
-| QMoveAfter of Id.t located or_anti
-| QMoveBefore of Id.t located or_anti
+| QMoveAfter of Id.t CAst.t or_anti
+| QMoveBefore of Id.t CAst.t or_anti
 | QMoveFirst
 | QMoveLast
 
-type move_location = move_location_r located
+type move_location = move_location_r CAst.t
 
-type pose = (Id.t located or_anti option * Constrexpr.constr_expr) located
+type pose = (Id.t CAst.t or_anti option * Constrexpr.constr_expr) CAst.t
 
 type assertion_r =
 | QAssertType of intro_pattern option * Constrexpr.constr_expr * raw_tacexpr option
-| QAssertValue of Id.t located or_anti * Constrexpr.constr_expr
+| QAssertValue of Id.t CAst.t or_anti * Constrexpr.constr_expr
 
-type assertion = assertion_r located
+type assertion = assertion_r CAst.t