diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 39 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 6 |
3 files changed, 36 insertions, 11 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 829556a71e..87609296bc 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(None, List.map snd recsl)) + (Vernacexpr.VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 1a8ec6d6f6..14b79d73ed 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1380,13 +1380,38 @@ and tactic_of_value ist vle = extra = TacStore.set ist.extra f_trace []; } in let tac = name_if_glob appl (eval_tactic ist t) in Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac) - | VFun (_, _, _,vars,_) -> - let numargs = List.length vars in - Tacticals.New.tclZEROMSG - (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++ - Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++ - Pp.str (String.plural numargs "variable") ++ Pp.str " " ++ - pr_enum Name.print vars ++ Pp.str ".") + | VFun (appl,_,vmap,vars,_) -> + let tactic_nm = + match appl with + UnnamedAppl -> "An unnamed user-defined tactic" + | GlbAppl apps -> + let nms = List.map (fun (kn,_) -> Names.KerName.to_string kn) apps in + match nms with + [] -> assert false + | kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *) + in + let numargs = List.length vars in + let givenargs = + List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in + let numgiven = List.length givenargs in + Tacticals.New.tclZEROMSG + (Pp.str tactic_nm ++ Pp.str " was not fully applied:" ++ spc() ++ + (match numargs with + 0 -> assert false + | 1 -> + Pp.str "There is a missing argument for variable " ++ + (Name.print (List.hd vars)) + | _ -> Pp.str "There are missing arguments for variables " ++ + pr_enum Name.print vars) ++ Pp.pr_comma () ++ + match numgiven with + 0 -> + Pp.str "no arguments at all were provided." + | 1 -> + Pp.str "an argument was provided for variable " ++ + Pp.str (List.hd givenargs) ++ Pp.str "." + | _ -> + Pp.str "arguments were provided for variables " ++ + pr_enum Pp.str givenargs ++ Pp.str ".") | VRec _ -> Tacticals.New.tclZEROMSG (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 diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 7385ed84c7..3efb7b9147 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -551,9 +551,9 @@ GEXTEND Gram | IDENT "Canonical"; qid = Constr.global; d = G_vernac.def_body -> let s = coerce_reference_to_id qid in - Vernacexpr.VernacDefinition - ((Some Decl_kinds.Global,Decl_kinds.CanonicalStructure), - ((Loc.tag s),None),(d )) + Vernacexpr.VernacLocal(false,Vernacexpr.VernacDefinition + ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), + ((Loc.tag s),None),(d ))) ]]; END |