From 5cd0310f061b5eb1a631a0fff0ee7eb9674a11c3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 Apr 2016 14:13:14 +0200
Subject: Removing "exact" from the tactic AST.

---
 ltac/extraargs.ml4 | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'ltac/extraargs.ml4')

diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index 0bddcc9fdd..9a2a176cbf 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -15,6 +15,7 @@ open Constrarg
 open Pcoq.Prim
 open Pcoq.Constr
 open Names
+open Tacmach
 open Tacexpr
 open Taccoerce
 open Tacinterp
@@ -175,6 +176,16 @@ ARGUMENT EXTEND lglob
   [ lconstr(c) ] -> [ c ]
 END
 
+let interp_casted_constr ist gl c =
+  interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c
+
+ARGUMENT EXTEND casted_constr
+  TYPED AS constr
+  PRINTED BY pr_gen
+  INTERPRETED BY interp_casted_constr
+  [ constr(c) ] -> [ c ]
+END
+
 type 'id gen_place= ('id * hyp_location_flag,unit) location
 
 type loc_place = Id.t Loc.located gen_place
-- 
cgit v1.2.3


From 3206bf597d63066d9d9f8adfd0fe76e3c1c97e4d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 May 2016 00:12:19 +0200
Subject: Removing "rename" from the tactic AST.

---
 ltac/extraargs.ml4 | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'ltac/extraargs.ml4')

diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index 9a2a176cbf..e6d0a9c69c 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -236,6 +236,14 @@ ARGUMENT EXTEND hloc
 
  END
 
+let pr_rename _ _ _ (n, m) = Nameops.pr_id n ++ str " into " ++ Nameops.pr_id m
+
+ARGUMENT EXTEND rename
+  TYPED AS ident * ident
+  PRINTED BY pr_rename
+| [ ident(n) "into" ident(m) ] -> [ (n, m) ]
+END
+
 (* Julien: Mise en commun des differentes version de replace with in by *)
 
 let pr_by_arg_tac _prc _prlc prtac opt_c =
-- 
cgit v1.2.3