More precise type for quotation entries.

3 files changed, 36 insertions, 47 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index e3d48f75ca..e5847119e1 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -326,7 +326,7 @@ GEXTEND Gram
     [ [ n = Prim.natural -> Loc.tag ~loc:!@loc n ] ]
   ;
   q_ident:
-    [ [ id = ident_or_anti -> Tac2quote.of_anti Tac2quote.of_ident id ] ]
+    [ [ id = ident_or_anti -> id ] ]
   ;
   qhyp:
     [ [ x = anti -> x
@@ -347,7 +347,7 @@ GEXTEND Gram
     ] ]
   ;
   q_bindings:
-    [ [ bl = with_bindings -> Tac2quote.of_bindings bl ] ]
+    [ [ bl = with_bindings -> bl ] ]
   ;
   intropatterns:
     [ [ l = LIST0 nonsimple_intropattern -> Loc.tag ~loc:!@loc l ]]
@@ -417,10 +417,10 @@ GEXTEND Gram
     ] ]
   ;
   q_intropatterns:
-    [ [ ipat = intropatterns -> Tac2quote.of_intro_patterns ipat ] ]
+    [ [ ipat = intropatterns -> ipat ] ]
   ;
   q_intropattern:
-    [ [ ipat = simple_intropattern -> Tac2quote.of_intro_pattern ipat ] ]
+    [ [ ipat = simple_intropattern -> ipat ] ]
   ;
   nat_or_anti:
     [ [ n = lnatural -> QExpr n
@@ -487,7 +487,7 @@ GEXTEND Gram
     ] ]
   ;
   q_clause:
-    [ [ cl = clause -> Tac2quote.of_clause cl ] ]
+    [ [ cl = clause -> cl ] ]
   ;
   concl_occ:
     [ [ "*"; occs = occs -> occs
@@ -506,7 +506,7 @@ GEXTEND Gram
     ] ]
   ;
   q_induction_clause:
-    [ [ cl = induction_clause -> Tac2quote.of_induction_clause cl ] ]
+    [ [ cl = induction_clause -> cl ] ]
   ;
   orient:
     [ [ "->" -> Loc.tag ~loc:!@loc (Some true)
@@ -539,7 +539,7 @@ GEXTEND Gram
     ] ]
   ;
   q_rewriting:
-    [ [ r = oriented_rewriter -> Tac2quote.of_rewriting r ] ]
+    [ [ r = oriented_rewriter -> r ] ]
   ;
   tactic_then_last:
     [ [ "|"; lta = LIST0 OPT tac2expr LEVEL "6" SEP "|" -> lta
@@ -556,10 +556,10 @@ GEXTEND Gram
     ] ]
   ;
   q_dispatch:
-    [ [ d = tactic_then_gen -> Tac2quote.of_dispatch (Loc.tag ~loc:!@loc d) ] ]
+    [ [ d = tactic_then_gen -> Loc.tag ~loc:!@loc d ] ]
   ;
   q_occurrences:
-    [ [ occs = occs -> Tac2quote.of_occurrences occs ] ]
+    [ [ occs = occs -> occs ] ]
   ;
 END
 
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 0415b6f15f..bec1761120 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -14,6 +14,7 @@ open Geninterp
 open Tac2env
 open Tac2expr
 open Tac2interp
+open Tac2entries.Pltac
 open Proofview.Notations
 
 (** Standard values *)
@@ -868,20 +869,12 @@ end
 let () = add_scope "tactic" begin function
 | [] ->
   (** Default to level 5 parsing *)
-  let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, 5) in
+  let scope = Extend.Aentryl (tac2expr, 5) in
   let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | [SexprInt (loc, n)] ->
   let () = if n < 0 || n > 6 then scope_fail () in
-  let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, n) in
-  let act tac = tac in
-  Tac2entries.ScopeRule (scope, act)
-| _ -> scope_fail ()
-end
-
-let () = add_scope "ident" begin function
-| [] ->
-  let scope = Extend.Aentry Tac2entries.Pltac.q_ident in
+  let scope = Extend.Aentryl (tac2expr, n) in
   let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
@@ -895,27 +888,21 @@ let () = add_scope "thunk" begin function
 | _ -> scope_fail ()
 end
 
-let () = add_scope "bindings" begin function
-| [] ->
-  let scope = Extend.Aentry Tac2entries.Pltac.q_bindings in
-  let act tac = tac in
-  Tac2entries.ScopeRule (scope, act)
-| _ -> scope_fail ()
-end
-
-let add_expr_scope name entry =
+let add_expr_scope name entry f =
   add_scope name begin function
-  | [] -> Tac2entries.ScopeRule (Extend.Aentry entry, (fun e -> e))
+  | [] -> Tac2entries.ScopeRule (Extend.Aentry entry, f)
   | _ -> scope_fail ()
   end
 
-let () = add_expr_scope "intropattern" Tac2entries.Pltac.q_intropattern
-let () = add_expr_scope "intropatterns" Tac2entries.Pltac.q_intropatterns
-let () = add_expr_scope "induction_clause" Tac2entries.Pltac.q_induction_clause
-let () = add_expr_scope "rewriting" Tac2entries.Pltac.q_rewriting
-let () = add_expr_scope "clause" Tac2entries.Pltac.q_clause
-let () = add_expr_scope "occurrences" Tac2entries.Pltac.q_occurrences
-let () = add_expr_scope "dispatch" Tac2entries.Pltac.q_dispatch
+let () = add_expr_scope "ident" q_ident (fun id -> Tac2quote.of_anti Tac2quote.of_ident id)
+let () = add_expr_scope "bindings" q_bindings Tac2quote.of_bindings
+let () = add_expr_scope "intropattern" q_intropattern Tac2quote.of_intro_pattern
+let () = add_expr_scope "intropatterns" q_intropatterns Tac2quote.of_intro_patterns
+let () = add_expr_scope "induction_clause" q_induction_clause Tac2quote.of_induction_clause
+let () = add_expr_scope "rewriting" q_rewriting Tac2quote.of_rewriting
+let () = add_expr_scope "clause" q_clause Tac2quote.of_clause
+let () = add_expr_scope "occurrences" q_occurrences Tac2quote.of_occurrences
+let () = add_expr_scope "dispatch" q_dispatch Tac2quote.of_dispatch
 
 let () = add_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr
 let () = add_generic_scope "open_constr" Pcoq.Constr.constr Stdarg.wit_open_constr
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index cf6cdfa74b..667378030a 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -55,15 +55,17 @@ module Pltac :
 sig
 val tac2expr : raw_tacexpr Pcoq.Gram.entry
 
-(** Quoted entries. They directly return an Ltac2 expression *)
-
-val q_ident : raw_tacexpr Pcoq.Gram.entry
-val q_bindings : raw_tacexpr Pcoq.Gram.entry
-val q_intropattern : raw_tacexpr Pcoq.Gram.entry
-val q_intropatterns : raw_tacexpr Pcoq.Gram.entry
-val q_induction_clause : raw_tacexpr Pcoq.Gram.entry
-val q_rewriting : raw_tacexpr Pcoq.Gram.entry
-val q_clause : raw_tacexpr Pcoq.Gram.entry
-val q_dispatch : raw_tacexpr Pcoq.Gram.entry
-val q_occurrences : raw_tacexpr Pcoq.Gram.entry
+(** Quoted entries. To be used for complex notations. *)
+
+open Tac2qexpr
+
+val q_ident : Id.t located or_anti Pcoq.Gram.entry
+val q_bindings : bindings Pcoq.Gram.entry
+val q_intropattern : intro_pattern Pcoq.Gram.entry
+val q_intropatterns : intro_pattern list located Pcoq.Gram.entry
+val q_induction_clause : induction_clause Pcoq.Gram.entry
+val q_rewriting : rewriting Pcoq.Gram.entry
+val q_clause : clause Pcoq.Gram.entry
+val q_dispatch : dispatch Pcoq.Gram.entry
+val q_occurrences : occurrences Pcoq.Gram.entry
 end