From 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 14 Feb 2018 06:57:40 +0100 Subject: [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. --- vernac/auto_ind_decl.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'vernac/auto_ind_decl.ml') 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 ]); (* -- cgit v1.2.3