diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 10 | ||||
| -rw-r--r-- | vernac/classes.ml | 8 | ||||
| -rw-r--r-- | vernac/himsg.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 8 | ||||
| -rw-r--r-- | vernac/vernacentries.mli | 2 |
5 files changed, 16 insertions, 16 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 2879feba7..1a6b4dcdb 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -86,12 +86,12 @@ let destruct_on c = destruct false None c None None let destruct_on_using c id = destruct false None c - (Some (Loc.tag @@ IntroOrPattern [[Loc.tag @@ IntroNaming IntroAnonymous]; - [Loc.tag @@ IntroNaming (IntroIdentifier id)]])) + (Some (CAst.make @@ IntroOrPattern [[CAst.make @@ IntroNaming IntroAnonymous]; + [CAst.make @@ IntroNaming (IntroIdentifier id)]])) None let destruct_on_as c l = - destruct false None c (Some (Loc.tag l)) None + destruct false None c (Some (CAst.make l)) None let inj_flags = Some { Equality.keep_proof_equalities = true; (* necessary *) @@ -620,8 +620,8 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). Proofview.Goal.enter begin fun gl -> let fresht = fresh_id (Id.of_string "Z") gl in destruct_on_as (EConstr.mkVar freshz) - (IntroOrPattern [[Loc.tag @@ IntroNaming (IntroIdentifier fresht); - Loc.tag @@ IntroNaming (IntroIdentifier freshz)]]) + (IntroOrPattern [[CAst.make @@ IntroNaming (IntroIdentifier fresht); + CAst.make @@ IntroNaming (IntroIdentifier freshz)]]) end ]); (* diff --git a/vernac/classes.ml b/vernac/classes.ml index 192cc8a55..e074e44a4 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -229,8 +229,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) | Some (Inl props) -> let get_id = function - | Ident id' -> id' - | Qualid (loc,id') -> (Loc.tag ?loc @@ snd (repr_qualid id')) + | Ident (loc, id') -> CAst.(make ?loc @@ id') + | Qualid (loc,id') -> CAst.(make ?loc @@ snd (repr_qualid id')) in let props, rest = List.fold_left @@ -238,7 +238,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) if is_local_assum decl then try let is_id (id', _) = match RelDecl.get_name decl, get_id id' with - | Name id, (_, id') -> Id.equal id id' + | Name id, {CAst.v=id'} -> Id.equal id id' | Anonymous, _ -> false in let (loc_mid, c) = @@ -247,7 +247,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let rest' = List.filter (fun v -> not (is_id v)) rest in - let (loc, mid) = get_id loc_mid in + let {CAst.loc;v=mid} = get_id loc_mid in List.iter (fun (n, _, x) -> if Name.equal n (Name mid) then Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 131b1fab6..249e7893c 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1015,8 +1015,8 @@ let explain_not_a_class env c = let c = EConstr.to_constr Evd.empty c in pr_constr_env env Evd.empty c ++ str" is not a declared type class." -let explain_unbound_method env cid id = - str "Unbound method name " ++ Id.print (snd id) ++ spc () ++ +let explain_unbound_method env cid { CAst.v = id } = + str "Unbound method name " ++ Id.print (id) ++ spc () ++ str"of class" ++ spc () ++ pr_global cid ++ str "." let pr_constr_exprs exprs = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7764920d9..b3eb13fb7 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -907,7 +907,7 @@ let vernac_set_used_variables e = (str "Unknown variable: " ++ Id.print id)) l; let _, to_clear = Proof_global.set_used_variables l in - let to_clear = List.map snd to_clear in + let to_clear = List.map (fun x -> x.CAst.v) to_clear in Proof_global.with_current_proof begin fun _ p -> if List.is_empty to_clear then (p, ()) else @@ -1860,8 +1860,8 @@ let vernac_search ~atts s gopt r = let vernac_locate = function | LocateAny (AN qid) -> print_located_qualid qid | LocateTerm (AN qid) -> print_located_term qid - | LocateAny (ByNotation (_, (ntn, sc))) (** TODO : handle Ltac notations *) - | LocateTerm (ByNotation (_, (ntn, sc))) -> + | LocateAny (ByNotation { CAst.v=(ntn, sc)}) (** TODO : handle Ltac notations *) + | LocateTerm (ByNotation { CAst.v=(ntn, sc)}) -> let _, env = Pfedit.get_current_context () in Notation.locate_notation (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc @@ -2259,7 +2259,7 @@ let with_fail st b f = | _ -> assert false end -let interp ?(verbosely=true) ?proof ~st (loc,c) = +let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} = let orig_univ_poly = Flags.is_universe_polymorphism () in let orig_program_mode = Flags.is_program_mode () in let flags f atts = diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 13ecaf37b..f6199e820 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -20,7 +20,7 @@ val vernac_require : val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - st:Vernacstate.t -> Vernacexpr.vernac_control Loc.located -> Vernacstate.t + st:Vernacstate.t -> Vernacexpr.vernac_control CAst.t -> Vernacstate.t (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name |