aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/ocaml.ml34
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/ltac/tacinterp.ml39
-rw-r--r--plugins/micromega/persistent_cache.ml4
-rw-r--r--plugins/romega/const_omega.ml2
-rw-r--r--plugins/ssr/ssrvernac.ml46
6 files changed, 71 insertions, 16 deletions
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 9cbc3fd713..5d0f9c167e 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -100,11 +100,41 @@ let pp_global k r = str (str_global k r)
let pp_modname mp = str (Common.pp_module mp)
+(* grammar from OCaml 4.06 manual, "Prefix and infix symbols" *)
+
+let infix_symbols =
+ ['=' ; '<' ; '>' ; '@' ; '^' ; ';' ; '&' ; '+' ; '-' ; '*' ; '/' ; '$' ; '%' ]
+let operator_chars =
+ [ '!' ; '$' ; '%' ; '&' ; '*' ; '+' ; '-' ; '.' ; '/' ; ':' ; '<' ; '=' ; '>' ; '?' ; '@' ; '^' ; '|' ; '~' ]
+
+(* infix ops in OCaml, but disallowed by preceding grammar *)
+
+let builtin_infixes =
+ [ "::" ; "," ]
+
+let substring_all_opchars s start stop =
+ let rec check_char i =
+ if i >= stop then true
+ else
+ List.mem s.[i] operator_chars && check_char (i+1)
+ in
+ check_char start
+
let is_infix r =
is_inline_custom r &&
(let s = find_custom r in
- let l = String.length s in
- l >= 2 && s.[0] == '(' && s.[l-1] == ')')
+ let len = String.length s in
+ len >= 3 &&
+ (* parenthesized *)
+ (s.[0] == '(' && s.[len-1] == ')' &&
+ let inparens = String.trim (String.sub s 1 (len - 2)) in
+ let inparens_len = String.length inparens in
+ (* either, begins with infix symbol, any remainder is all operator chars *)
+ (List.mem inparens.[0] infix_symbols && substring_all_opchars inparens 1 inparens_len) ||
+ (* or, starts with #, at least one more char, all are operator chars *)
+ (inparens.[0] == '#' && inparens_len >= 2 && substring_all_opchars inparens 1 inparens_len) ||
+ (* or, is an OCaml built-in infix *)
+ (List.mem inparens builtin_infixes)))
let get_infix r =
let s = find_custom r in
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/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 49ccb468c1..387a525141 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -149,7 +149,7 @@ let open_in f =
match read_key_elem inch with
| None -> ()
| Some (key,elem) ->
- Table.add htbl key elem ;
+ Table.replace htbl key elem ;
xload () in
try
(* Locking of the (whole) file while reading *)
@@ -195,7 +195,7 @@ let add t k e =
else
let fd = descr_of_out_channel outch in
begin
- Table.add tbl k e ;
+ Table.replace tbl k e ;
do_under_lock Write fd
(fun _ ->
Marshal.to_channel outch (k,e) [Marshal.No_sharing] ;
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 337510ef1f..0d491d92bd 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -155,7 +155,7 @@ let mk_list univ typ l =
loop l
let mk_plist =
- let type1lev = Universes.new_univ_level (Global.current_dirpath ()) in
+ let type1lev = Universes.new_univ_level () in
fun l -> mk_list type1lev mkProp l
let mk_list = mk_list Univ.Level.set
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 10:38:30 +0000