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

(limited to 'plugins/micromega')

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 52822e444a..168105e8fd 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1991,7 +1991,7 @@ let micromega_gen
 
        let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
        let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
-       let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
+       let ipat_of_name id = Some (CAst.make @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
        let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in
        let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in 
 
@@ -2106,7 +2106,7 @@ let micromega_genr prover tac =
 
        let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
        let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
-       let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
+       let ipat_of_name id = Some (CAst.make @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
        let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in
        let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in 
        
-- 
cgit v1.2.3