Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at

internalization time.

6 files changed, 62 insertions, 35 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 2c4f84397..1d560e699 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -139,6 +139,7 @@ Pputils
 Stdarg
 Constrarg
 Constrexpr_ops
+Genintern
 Notation_ops
 Topconstr
 Notation
@@ -148,7 +149,6 @@ Impargs
 Syntax_def
 Implicit_quantifiers
 Smartlocate
-Genintern
 Constrintern
 Modintern
 Constrextern
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index cc4655315..fde5a11f1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -531,21 +531,7 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
   let rec aux (terms,binderopt as subst') (renaming,env) c =
     let subinfos = renaming,{env with tmp_scope = None} in
     match c with
-    | NVar id ->
-      begin
-	(* subst remembers the delimiters stack in the interpretation *)
-	(* of the notations *)
-	try
-	  let (a,(scopt,subscopes)) = Id.Map.find id terms in
-	  intern {env with tmp_scope = scopt;
-		    scopes = subscopes @ env.scopes} a
-	with Not_found ->
-	try
-	  GVar (loc, Id.Map.find id renaming)
-	with Not_found ->
-	  (* Happens for local notation joint with inductive/fixpoint defs *)
-	  GVar (loc,id)
-      end
+    | NVar id -> subst_var subst' (renaming, env) id
     | NList (x,_,iter,terminator,lassoc) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
@@ -558,11 +544,34 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
 	List.fold_right fold (if lassoc then List.rev l else l) termin
       with Not_found ->
           anomaly (Pp.str "Inconsistent substitution of recursive notation"))
-    | NHole (Evar_kinds.BinderType (Name id as na)) ->
-      let na =
-        try snd (coerce_to_name (fst (Id.Map.find id terms)))
-        with Not_found -> na in
-      GHole (loc,Evar_kinds.BinderType na,None)
+    | NHole (knd, arg) ->
+      let knd = match knd with
+      | Evar_kinds.BinderType (Name id as na) ->
+        let na =
+          try snd (coerce_to_name (fst (Id.Map.find id terms)))
+          with Not_found -> na
+        in
+        Evar_kinds.BinderType na
+      | _ -> knd
+      in
+      let arg = match arg with
+      | None -> None
+      | Some arg ->
+        let open Tacexpr in
+        let open Genarg in
+        let mk_env id (c, (tmp_scope, subscopes)) accu =
+          let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
+          let gc = intern nenv c in
+          let c = ConstrMayEval (Genredexpr.ConstrTerm (gc, Some c)) in
+          ((loc, id), c) :: accu
+        in
+        let bindings = Id.Map.fold mk_env terms [] in
+        let body = TacArg (loc, TacGeneric arg) in
+        let tac = TacLetIn (false, bindings, body) in
+        let arg = in_gen (glbwit Constrarg.wit_tactic) tac in
+        Some arg
+      in
+      GHole (loc, knd, arg)
     | NBinderList (x,_,iter,terminator) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
@@ -586,6 +595,19 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
     | t ->
       glob_constr_of_notation_constr_with_binders loc
         (traverse_binder subst) (aux subst') subinfos t
+  and subst_var (terms, binderopt) (renaming, env) id =
+    (* subst remembers the delimiters stack in the interpretation *)
+    (* of the notations *)
+    try
+      let (a,(scopt,subscopes)) = Id.Map.find id terms in
+      intern {env with tmp_scope = scopt;
+                scopes = subscopes @ env.scopes} a
+    with Not_found ->
+    try
+      GVar (loc, Id.Map.find id renaming)
+    with Not_found ->
+      (* Happens for local notation joint with inductive/fixpoint defs *)
+      GVar (loc,id)
   in aux (terms,None) infos c
 
 let split_by_type ids =
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 7f14fe42b..c9a031526 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,3 +1,5 @@
+Stdarg
+Constrarg
 Genintern
 Constrexpr_ops
 Notation_ops
@@ -16,5 +18,3 @@ Constrextern
 Coqlib
 Discharge
 Declare
-Stdarg
-Constrarg
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ce9deb0db..57fc15f8e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -104,7 +104,7 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function
       GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
   | NCast (c,k) -> GCast (loc,f e c,Miscops.map_cast_type (f e) k)
   | NSort x -> GSort (loc,x)
-  | NHole x  -> GHole (loc, x, None)
+  | NHole (x, arg)  -> GHole (loc, x, arg)
   | NPatVar n -> GPatVar (loc,(false,n))
   | NRef x -> GRef (loc,x)
 
@@ -287,7 +287,7 @@ let notation_constr_and_vars_of_glob_constr a =
       NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
   | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k)
   | GSort (_,s) -> NSort s
-  | GHole (_,w,_) -> NHole w
+  | GHole (_,w,arg) -> NHole (w, arg)
   | GRef (_,r) -> NRef r
   | GPatVar (_,(_,n)) -> NPatVar n
   | GEvar _ ->
@@ -465,14 +465,16 @@ let rec subst_notation_constr subst bound raw =
 
   | NPatVar _ | NSort _ -> raw
 
-  | NHole (Evar_kinds.ImplicitArg (ref,i,b)) ->
-      let ref',t = subst_global subst ref in
-	if ref' == ref then raw else
-	  NHole (Evar_kinds.InternalHole)
-  | NHole (Evar_kinds.BinderType _ |Evar_kinds.QuestionMark _
-	  |Evar_kinds.CasesType |Evar_kinds.InternalHole
-	  |Evar_kinds.TomatchTypeParameter _ |Evar_kinds.GoalEvar
-	  |Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _) -> raw
+  | NHole (knd, solve) ->
+    let nknd = match knd with
+    | Evar_kinds.ImplicitArg (ref, i, b) ->
+      let nref, _ = subst_global subst ref in
+      if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b)
+    | _ -> knd
+    in
+    let nsolve = Option.smartmap (Genintern.generic_substitute subst) solve in
+    if nsolve == solve && nknd = knd then raw
+    else NHole (nknd, nsolve)
 
   | NCast (r1,k) ->
       let r1' = subst_notation_constr subst bound r1 in
@@ -500,7 +502,7 @@ let abstract_return_type_context_glob_constr =
 
 let abstract_return_type_context_notation_constr =
   abstract_return_type_context snd
-    (fun na c -> NLambda(na,NHole Evar_kinds.InternalHole,c))
+    (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, None),c))
 
 exception No_match
 
diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index ac5e0f5f9..daf605ab2 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -24,7 +24,7 @@ type notation_constr =
   | NRef of global_reference
   | NVar of Id.t
   | NApp of notation_constr * notation_constr list
-  | NHole of Evar_kinds.t
+  | NHole of Evar_kinds.t * Genarg.glob_generic_argument option
   | NList of Id.t * Id.t * notation_constr * notation_constr * bool
   (** Part only in [glob_constr] *)
   | NLambda of Name.t * notation_constr * notation_constr
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b697d3635..712191a73 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1185,6 +1185,9 @@ and tactic_of_value ist vle =
       let tac = eval_tactic ist t in
       catch_error_tac trace tac
   | (VFun _|VRec _) -> Proofview.tclZERO (UserError ("" , str "A fully applied tactic is expected."))
+  else if has_type vle (topwit wit_tactic) then
+    let tac = out_gen (topwit wit_tactic) vle in
+    eval_tactic ist tac
   else Proofview.tclZERO (UserError ("" , str"Expression does not evaluate to a tactic."))
 
 and eval_value ist tac =