Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 5c581cf2 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'new_ide'

parents dd2d6f14 8a999dee
......@@ -31,7 +31,7 @@ void parse_options(int argc, char **argv) {
};
while (1) {
int option_index = 0;
char c = 0;
int c = 0;
c = getopt_long (argc, argv, "j:s:",
long_options, &option_index);
/* Detect the end of the options. */
......
......@@ -59,7 +59,10 @@ let subst_quant_list quant term_quant list_term : term =
match list_term, vsl with
| t :: lt_tl, v :: vsl_tl ->
let (ty_subst, _) =
Reduction_engine.first_order_matching (Svs.add v Svs.empty) [Term.t_var v] [t]
try
Reduction_engine.first_order_matching (Svs.add v Svs.empty) [Term.t_var v] [t]
with Reduction_engine.NoMatch _e ->
raise (Arg_trans (Format.asprintf "cannot match %a with %a" Pretty.print_term (Term.t_var v) Pretty.print_term t))
in
create_mvs lt_tl vsl_tl (Mvs.add v t acc)
(Ty.Mtv.union (fun _ _ y -> Some y) ty_subst acc_ty)
......@@ -70,7 +73,7 @@ let subst_quant_list quant term_quant list_term : term =
let (ty_subst, m_subst), variables_remaining =
try
create_mvs list_term vsl Mvs.empty Ty.Mtv.empty
with _ -> raise (Arg_trans ("subst_quant_list"))
with exn -> raise (Arg_trans (Format.asprintf "subst_quant_list: exception %a" Exn_printer.exn_printer exn))
in
try
let new_t = t_ty_subst ty_subst m_subst te in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment