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. --- proofs/proof_global.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs/proof_global.ml') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 15f34ccc6..d6c0e3341 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -207,7 +207,7 @@ let check_no_pending_proof () = let discard_gen id = pstates := List.filter (fun { pid = id' } -> not (Id.equal id id')) !pstates -let discard (loc,id) = +let discard {CAst.loc;v=id} = let n = List.length !pstates in discard_gen id; if Int.equal (List.length !pstates) n then @@ -297,13 +297,13 @@ let set_used_variables l = match entry with | LocalAssum (x,_) -> if Id.Set.mem x all_safe then orig - else (ctx, all_safe, (Loc.tag x)::to_clear) + else (ctx, all_safe, (CAst.make x)::to_clear) | LocalDef (x,bo, ty) as decl -> if Id.Set.mem x all_safe then orig else let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in if Id.Set.subset vars all_safe then (decl :: ctx, Id.Set.add x all_safe, to_clear) - else (ctx, all_safe, (Loc.tag x) :: to_clear) in + else (ctx, all_safe, (CAst.make x) :: to_clear) in let ctx, _, to_clear = Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in let to_clear = if !proof_using_auto_clear then to_clear else [] in -- cgit v1.2.3