Merge pull request #13 from ppedrot/coqpp-port

Port to coqpp.
coq-community · Nov 5, 2018 · bed487f · bed487f
2 parents c106362 + a6cadb0
commit bed487f
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 22 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -5,4 +5,3 @@ script:
 
 env:
   - COQ_VERSION=master
-  - COQ_VERSION=v8.9
diff --git a/_CoqProject b/_CoqProject
@@ -15,7 +15,7 @@ src/matcher.ml
 src/theory.ml
 src/print.ml
 src/aac_rewrite.ml
-src/aac.ml4
+src/aac.mlg
 src/aac_plugin.mlpack
 
 theories/Utils.v

diff --git a/src/aac.ml4 → src/aac.mlg b/src/aac.ml4 → src/aac.mlg
@@ -10,7 +10,8 @@
 
 DECLARE PLUGIN "aac_plugin"
 
-
+{
+
 open Ltac_plugin
 open Pcoq.Prim
 open Pcoq.Constr
@@ -19,61 +20,67 @@ 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 ]
-| [ ] -> [ [] ]
+}
+
+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 ]
+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 ]
+| [ "aac_reflexivity" ] -> { Proofview.V82.tactic aac_reflexivity }
 END
 
 TACTIC EXTEND _aac_normalise_
-| [ "aac_normalise" ] -> [ Proofview.V82.tactic 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) ]
+  { 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) ]
+  { 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) ]
+  { 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) ]
+  { 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) ]
+  { 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) ]
+  { Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~show:true c gl) }
 END