From 8018e923c75eb5504310864f821972f794b7d554 Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@google.com>
Date: Wed, 13 Feb 2019 20:40:51 -0500
Subject: New upstream version 8.8.0+1.gbp069dc3b

---
 src/aac.ml4 | 79 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 79 insertions(+)
 create mode 100644 src/aac.ml4

(limited to 'src/aac.ml4')

diff --git a/src/aac.ml4 b/src/aac.ml4
new file mode 100644
index 0000000..e879a69
--- /dev/null
+++ b/src/aac.ml4
@@ -0,0 +1,79 @@
+(***************************************************************************)
+(*  This is part of aac_tactics, it is distributed under the terms of the  *)
+(*         GNU Lesser General Public License version 3                     *)
+(*              (see file LICENSE for more details)                        *)
+(*                                                                         *)
+(*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
+(***************************************************************************)
+
+(** aac -- Reasoning modulo associativity and commutativity *)
+
+DECLARE PLUGIN "aac_plugin"
+
+      
+open Ltac_plugin
+open Pcoq.Prim
+open Pcoq.Constr
+open Stdarg
+open Aac_rewrite
+open Extraargs
+open Genarg
+
+ARGUMENT EXTEND aac_args  
+TYPED AS ((string * int) list ) 
+PRINTED BY pr_aac_args
+| [ "at" integer(n) aac_args(q) ] -> [ add "at" n q ]
+| [ "subst" integer(n) aac_args(q) ] -> [ add "subst" n q ]
+| [ "in_right" aac_args(q) ] -> [ add "in_right" 0 q ]
+| [ ] -> [ [] ]
+END
+
+let pr_constro _ _ _ = fun b ->
+  match b with
+    | None ->  Pp.str ""
+    | Some o -> Pp.str "<constr>"
+
+ARGUMENT EXTEND constro
+TYPED AS (constr option) 
+PRINTED BY pr_constro
+| [ "[" constr(c) "]" ] -> [ Some c ]
+| [ ] -> [ None ]
+END
+
+TACTIC EXTEND _aac_reflexivity_
+| [ "aac_reflexivity" ] -> [ Proofview.V82.tactic aac_reflexivity ]
+END
+
+TACTIC EXTEND _aac_normalise_
+| [ "aac_normalise" ] -> [ Proofview.V82.tactic aac_normalise ]
+END
+
+TACTIC EXTEND _aac_rewrite_
+| [ "aac_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
+  [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true c gl) ]
+END
+ 
+TACTIC EXTEND _aac_pattern_
+| [ "aac_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
+  [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~abort:true c gl) ]
+END
+
+TACTIC EXTEND _aac_instances_
+| [ "aac_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
+  [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~show:true c gl) ]
+END
+
+TACTIC EXTEND _aacu_rewrite_
+| [ "aacu_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
+  [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false c gl) ]
+END
+ 
+TACTIC EXTEND _aacu_pattern_
+| [ "aacu_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
+  [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~abort:true c gl) ]
+END
+
+TACTIC EXTEND _aacu_instances_
+| [ "aacu_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
+  [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~show:true c gl) ]
+END
-- 
cgit v1.2.3