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.
---
 plugins/funind/invfun.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b858e78d0e..2743a8a2f9 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -240,7 +240,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
       List.map
 	(fun decl ->
 	   List.map
-	     (fun id -> Loc.tag @@ IntroNaming (IntroIdentifier id))
+             (fun id -> CAst.make @@ IntroNaming (IntroIdentifier id))
 	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl)))))
 	)
 	branches
@@ -256,7 +256,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
       (* We get the identifiers of this branch *)
       let pre_args =
       	List.fold_right
-      	  (fun (_,pat) acc ->
+          (fun {CAst.v=pat} acc ->
       	     match pat with
 	       | IntroNaming (IntroIdentifier id) -> id::acc
       	       | _ -> anomaly (Pp.str "Not an identifier.")
-- 
cgit v1.2.3