aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/gen_principle.ml71
-rw-r--r--plugins/ltac/extratactics.mlg12
-rw-r--r--plugins/ltac/g_auto.mlg2
-rw-r--r--plugins/ltac/tacentries.ml52
-rw-r--r--plugins/ltac/tacinterp.ml8
-rw-r--r--plugins/micromega/.ocamlformat1
-rw-r--r--plugins/micromega/.ocamlformat-ignore1
-rw-r--r--plugins/ssr/ssrcommon.ml2
8 files changed, 73 insertions, 76 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 446026c4c8..d38c3c869b 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -39,7 +39,7 @@ let build_newrecursive lnameargsardef =
List.fold_left
(fun (env,impls) { Vernacexpr.fname={CAst.v=recname}; binders; rtype } ->
let arityc = Constrexpr_ops.mkCProdN binders rtype in
- let arity,ctx = Constrintern.interp_type env0 sigma arityc in
+ let arity,_ctx = Constrintern.interp_type env0 sigma arityc in
let evd = Evd.from_env env0 in
let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd binders in
let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in
@@ -164,7 +164,7 @@ let prepare_body { Vernacexpr.binders } rt =
let fun_args,rt' = chop_rlambda_n n rt in
(fun_args,rt')
-let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
+let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) old_princ_type sorts funs _i proof_tac hook =
(* First we get the type of the old graph principle *)
let mutr_nparams = (Tactics.compute_elim_sig !evd (EConstr.of_constr old_princ_type)).Tactics.nparams in
(* let time1 = System.get_time () in *)
@@ -199,7 +199,7 @@ let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_
(* end; *)
let open Proof_global in
- let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+ let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false) lemma in
match entries with
| [entry] ->
entry, hook
@@ -235,7 +235,6 @@ let change_property_sort evd toSort princ princName =
(List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_info.Tactics.params)
let generate_functional_principle (evd: Evd.evar_map ref)
- interactive_proof
old_princ_type sorts new_princ_name funs i proof_tac
=
try
@@ -283,27 +282,25 @@ let generate_functional_principle (evd: Evd.evar_map ref)
register_with_sort Sorts.InSet
in
let entry, hook =
- build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
+ build_functional_principle evd old_princ_type new_sorts funs i
proof_tac hook
in
(* Pr 1278 :
Don't forget to close the goal if an error is raised !!!!
*)
let uctx = Evd.evar_universe_context sigma in
- let hook_data = hook, uctx, [] in
- let _ : Names.GlobRef.t = DeclareDef.declare_definition
- ~name:new_princ_name ~hook_data
+ let _ : Names.GlobRef.t = DeclareDef.declare_entry
+ ~name:new_princ_name ~hook
~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
~kind:Decls.(IsProof Theorem)
- ~ubind:UnivNames.empty_binders
~impargs:[]
- entry in
+ ~uctx entry in
()
with e when CErrors.noncritical e ->
raise (Defining_principle e)
let generate_principle (evd:Evd.evar_map ref) pconstants on_error
- is_general do_built fix_rec_l recdefs interactive_proof
+ is_general do_built fix_rec_l recdefs
(continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int ->
Tacmach.tactic) : unit =
let names = List.map (function { Vernacexpr.fname = {CAst.v=name} } -> name) fix_rec_l in
@@ -336,7 +333,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in
let _ =
List.map_i
- (fun i x ->
+ (fun i _x ->
let env = Global.env () in
let princ = Indrec.lookup_eliminator env (ind_kn,i) (Sorts.InProp) in
let evd = ref (Evd.from_env env) in
@@ -347,7 +344,6 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
let princ_type = EConstr.Unsafe.to_constr princ_type in
generate_functional_principle
evd
- interactive_proof
princ_type
None
None
@@ -375,7 +371,6 @@ let register_struct is_rec fixpoint_exprl =
| None ->
CErrors.user_err ~hdr:"Function" Pp.(str "Body of Function must be given") in
ComDefinition.do_definition
- ~program_mode:false
~name:fname.CAst.v
~poly:false
~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
@@ -413,7 +408,7 @@ let register_struct is_rec fixpoint_exprl =
None,evd,List.rev rev_pconstants
let generate_correction_proof_wf f_ref tcc_lemma_ref
- is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+ is_mes functional_ref eq_ref rec_arg_num rec_arg_type relation
(_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Tacmach.tactic =
Functional_principles_proofs.prove_principle_for_gen
(f_ref,functional_ref,eq_ref)
@@ -431,7 +426,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
res = fv \rightarrow graph\ x_1\ldots x_n\ res\] decomposed as the context and the conclusion
*)
-let generate_type evd g_to_f f graph i =
+let generate_type evd g_to_f f graph =
let open Context.Rel.Declaration in
let open EConstr in
let open EConstr.Vars in
@@ -499,7 +494,7 @@ let generate_type evd g_to_f f graph i =
WARNING: while convertible, [type_of body] and [type] can be non equal
*)
let find_induction_principle evd f =
- let f_as_constant,u = match EConstr.kind !evd f with
+ let f_as_constant, _u = match EConstr.kind !evd f with
| Constr.Const c' -> c'
| _ -> CErrors.user_err Pp.(str "Must be used with a function")
in
@@ -546,7 +541,7 @@ let rec generate_fresh_id x avoid i =
let id = Namegen.next_ident_away_in_goal x (Id.Set.of_list avoid) in
id::(generate_fresh_id x (id::avoid) (pred i))
-let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic =
+let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i : Tacmach.tactic =
let open Constr in
let open EConstr in
let open Context.Rel.Declaration in
@@ -1141,7 +1136,7 @@ let get_funs_constant mp =
to prevent Reset strange thing
*)
let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in
- let l_params,l_fixes = List.split (List.map Term.decompose_lam l_bodies) in
+ let l_params, _l_fixes = List.split (List.map Term.decompose_lam l_bodies) in
(* all the parameters must be equal*)
let _check_params =
let first_params = List.hd l_params in
@@ -1241,7 +1236,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
in
let entry, _hook =
try
- build_functional_principle ~opaque evd false
+ build_functional_principle ~opaque evd
first_type
(Array.of_list sorts)
this_block_funs
@@ -1262,7 +1257,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
let sorts = Array.of_list sorts in
List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types
in
- let first_princ_body,first_princ_type = Declare.(entry.proof_entry_body, entry.proof_entry_type) in
+ let first_princ_body = entry.Declare.proof_entry_body in
let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in
let other_result =
@@ -1292,7 +1287,6 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
let entry, _hook =
build_functional_principle
evd
- false
(List.nth other_princ_types (!i - 1))
(Array.of_list sorts)
this_block_funs
@@ -1331,9 +1325,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
let lemmas_types_infos =
Util.Array.map2_i
(fun i f_constr graph ->
- (* let const_of_f,u = destConst f_constr in *)
let (type_of_lemma_ctxt,type_of_lemma_concl,graph) =
- generate_type evd false f_constr graph i
+ generate_type evd false f_constr graph
in
let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
graphs_constr.(i) <- graph;
@@ -1368,7 +1361,7 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
)
in
let proving_tac =
- prove_fun_correct !evd funs_constr graphs_constr schemes lemmas_types_infos
+ prove_fun_correct !evd graphs_constr schemes lemmas_types_infos
in
Array.iteri
(fun i f_as_constant ->
@@ -1398,8 +1391,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
let lemmas_types_infos =
Util.Array.map2_i
(fun i f_constr graph ->
- let (type_of_lemma_ctxt,type_of_lemma_concl,graph) =
- generate_type evd true f_constr graph i
+ let (type_of_lemma_ctxt,type_of_lemma_concl,graph) =
+ generate_type evd true f_constr graph
in
let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
graphs_constr.(i) <- graph;
@@ -1415,7 +1408,7 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
in
let (kn,_) as graph_ind,u = (destInd !evd graphs_constr.(0)) in
- let mib,mip = Global.lookup_inductive graph_ind in
+ let mib, _mip = Global.lookup_inductive graph_ind in
let sigma, scheme =
(Indrec.build_mutual_induction_scheme (Global.env ()) !evd
(Array.to_list
@@ -1485,7 +1478,7 @@ let derive_inversion fix_names =
*)
List.iter (fun c -> ignore (find_Function_infos (fst c))) fix_names_as_constant ;
try
- let evd', lind =
+ let _evd', lind =
List.fold_right
(fun id (evd,l) ->
let evd,id =
@@ -1536,11 +1529,11 @@ let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf
in
let eq = Constrexpr_ops.mkCProdN args unbounded_eq in
let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type
- nb_args relation =
+ _nb_args relation =
try
pre_hook [fconst]
(generate_correction_proof_wf f_ref tcc_lemma_ref is_mes
- functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+ functional_ref eq_ref rec_arg_num rec_arg_type relation
);
derive_inversion [fname]
with e when CErrors.noncritical e ->
@@ -1562,7 +1555,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w
| None ->
begin
match args with
- | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],k,t)] -> t,x
+ | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],_k,t)] -> t,x
| _ -> CErrors.user_err (Pp.str "Recursive argument must be specified")
end
| Some wf_args ->
@@ -1570,7 +1563,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w
match
List.find
(function
- | Constrexpr.CLocalAssum(l,k,t) ->
+ | Constrexpr.CLocalAssum(l,_k,t) ->
List.exists
(function {CAst.v=Name id} -> Id.equal id wf_args | _ -> false)
l
@@ -1578,7 +1571,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w
)
args
with
- | Constrexpr.CLocalAssum(_,k,t) -> t,wf_args
+ | Constrexpr.CLocalAssum(_,_k,t) -> t,wf_args
| _ -> assert false
with Not_found -> assert false
in
@@ -1626,7 +1619,7 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
let lemma, _is_struct =
match fixpoint_exprl with
| [{ Vernacexpr.rec_order = Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)} } as fixpoint_expr] ->
- let { Vernacexpr.fname; univs; binders; rtype; body_def } as fixpoint_expr =
+ let { Vernacexpr.fname; univs = _; binders; rtype; body_def } as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -1645,13 +1638,12 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
register_built
fixpoint_exprl
recdefs
- true
in
if register_built
then register_wf interactive_proof fname.CAst.v rec_impls wf_rel wf_x.CAst.v using_lemmas binders rtype body pre_hook, false
else None, false
| [{ Vernacexpr.rec_order = Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)} } as fixpoint_expr] ->
- let { Vernacexpr.fname; univs; binders; rtype; body_def} as fixpoint_expr =
+ let { Vernacexpr.fname; univs = _; binders; rtype; body_def} as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -1672,7 +1664,6 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
register_built
fixpoint_exprl
recdefs
- true
in
if register_built
then register_mes interactive_proof fname.CAst.v rec_impls wf_mes wf_rel_opt
@@ -1690,7 +1681,7 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
let fixpoint_exprl = recompute_binder_list fixpoint_exprl in
let fix_names = List.map (function { Vernacexpr.fname } -> fname.CAst.v) fixpoint_exprl in
(* ok all the expressions are structural *)
- let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
+ let recdefs, _rec_impls = build_newrecursive fixpoint_exprl in
let is_rec = List.exists (is_rec fix_names) recdefs in
let lemma,evd,pconstants =
if register_built
@@ -1706,7 +1697,6 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
register_built
fixpoint_exprl
recdefs
- interactive_proof
(Functional_principles_proofs.prove_princ_for_struct evd interactive_proof);
if register_built then
begin derive_inversion fix_names; end;
@@ -2067,7 +2057,6 @@ let build_case_scheme fa =
*)
generate_functional_principle
(ref (Evd.from_env (Global.env ())))
- false
scheme_type
(Some ([|sorts|]))
(Some princ_name)
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 9b80cbd803..7b1aa7a07a 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -47,7 +47,7 @@ DECLARE PLUGIN "ltac_plugin"
let with_delayed_uconstr ist c tac =
let flags = {
- Pretyping.use_typeclasses = false;
+ Pretyping.use_typeclasses = Pretyping.NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -345,7 +345,7 @@ open EConstr
open Vars
let constr_flags () = {
- Pretyping.use_typeclasses = true;
+ Pretyping.use_typeclasses = Pretyping.UseTC;
Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
Pretyping.fail_evar = false;
Pretyping.expand_evars = true;
@@ -375,22 +375,22 @@ let refine_tac ist simple with_classes c =
TACTIC EXTEND refine
| [ "refine" uconstr(c) ] ->
- { refine_tac ist false true c }
+ { refine_tac ist false Pretyping.UseTC c }
END
TACTIC EXTEND simple_refine
| [ "simple" "refine" uconstr(c) ] ->
- { refine_tac ist true true c }
+ { refine_tac ist true Pretyping.UseTC c }
END
TACTIC EXTEND notcs_refine
| [ "notypeclasses" "refine" uconstr(c) ] ->
- { refine_tac ist false false c }
+ { refine_tac ist false Pretyping.NoUseTC c }
END
TACTIC EXTEND notcs_simple_refine
| [ "simple" "notypeclasses" "refine" uconstr(c) ] ->
- { refine_tac ist true false c }
+ { refine_tac ist true Pretyping.NoUseTC c }
END
(* Solve unification constraints using heuristics or fail if any remain *)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 3c30c881fb..b4527694ae 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -53,7 +53,7 @@ END
let eval_uconstrs ist cs =
let flags = {
- Pretyping.use_typeclasses = false;
+ Pretyping.use_typeclasses = Pretyping.NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4af5699317..4127d28bae 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -44,11 +44,11 @@ let coincide s pat off =
!break
let atactic n =
- if n = 5 then Aentry Pltac.binder_tactic
- else Aentryl (Pltac.tactic_expr, string_of_int n)
+ if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic
+ else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n)
type entry_name = EntryName :
- 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Extend.symbol -> entry_name
+ 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> entry_name
(** Quite ad-hoc *)
let get_tacentry n m =
@@ -57,8 +57,8 @@ let get_tacentry n m =
&& not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
&& not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
in
- if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Aself)
- else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Anext)
+ if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.self)
+ else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.next)
else EntryName (rawwit Tacarg.wit_tactic, atactic n)
let get_separator = function
@@ -140,23 +140,23 @@ let head_is_ident tg = match tg.tacgram_prods with
let rec prod_item_of_symbol lev = function
| Extend.Ulist1 s ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Alist1 e)
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1 e)
| Extend.Ulist0 s ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Alist0 e)
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0 e)
| Extend.Ulist1sep (s, sep) ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Alist1sep (e, Atoken (CLexer.terminal sep)))
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1sep e (Pcoq.Symbol.token (CLexer.terminal sep)) false)
| Extend.Ulist0sep (s, sep) ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Alist0sep (e, Atoken (CLexer.terminal sep)))
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0sep e (Pcoq.Symbol.token (CLexer.terminal sep)) false)
| Extend.Uopt s ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (OptArg typ), Aopt e)
+ EntryName (Rawwit (OptArg typ), Pcoq.Symbol.opt e)
| Extend.Uentry arg ->
let ArgT.Any tag = arg in
let wit = ExtraArg tag in
- EntryName (Rawwit wit, Extend.Aentry (genarg_grammar wit))
+ EntryName (Rawwit wit, Pcoq.Symbol.nterm (genarg_grammar wit))
| Extend.Uentryl (s, n) ->
let ArgT.Any tag = s in
assert (coincide (ArgT.repr tag) "tactic" 0);
@@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) state =
in
let prods = List.map map tg.tacgram_prods in
let rules = make_rule mkact prods in
- let r = ExtendRule (entry, (pos, [(None, None, [rules])])) in
+ let r = ExtendRule (entry, { pos; data=[(None, None, [rules])]}) in
([r], state)
let tactic_grammar =
@@ -399,23 +399,29 @@ let create_ltac_quotation name cast (e, l) =
in
let () = ltac_quotations := String.Set.add name !ltac_quotations in
let entry = match l with
- | None -> Aentry e
- | Some l -> Aentryl (e, string_of_int l)
+ | None -> Pcoq.Symbol.nterm e
+ | Some l -> Pcoq.Symbol.nterml e (string_of_int l)
in
(* let level = Some "1" in *)
let level = None in
let assoc = None in
let rule =
- Next (Next (Next (Next (Next (Stop,
- Atoken (CLexer.terminal name)),
- Atoken (CLexer.terminal ":")),
- Atoken (CLexer.terminal "(")),
- entry),
- Atoken (CLexer.terminal ")"))
+ Pcoq.(
+ Rule.next
+ (Rule.next
+ (Rule.next
+ (Rule.next
+ (Rule.next
+ Rule.stop
+ (Symbol.token (CLexer.terminal name)))
+ (Symbol.token (CLexer.terminal ":")))
+ (Symbol.token (CLexer.terminal "(")))
+ entry)
+ (Symbol.token (CLexer.terminal ")")))
in
let action _ v _ _ _ loc = cast (Some loc, v) in
- let gram = (level, assoc, [Rule (rule, action)]) in
- Pcoq.grammar_extend Pltac.tactic_arg (None, [gram])
+ let gram = (level, assoc, [Pcoq.Production.make rule action]) in
+ Pcoq.grammar_extend Pltac.tactic_arg {pos=None; data=[gram]}
(** Command *)
@@ -759,7 +765,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
e
| Vernacextend.Arg_rules rules ->
let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
- let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in
+ let () = Pcoq.grammar_extend e {pos=None; data=[(None, None, rules)]} in
e
in
let (rpr, gpr, tpr) = arg.arg_printer in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9e0b9d3254..b0e26e1def 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -546,7 +546,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
(evd,c)
let constr_flags () = {
- use_typeclasses = true;
+ use_typeclasses = UseTC;
solve_unification_constraints = true;
fail_evar = true;
expand_evars = true;
@@ -564,7 +564,7 @@ let interp_constr = interp_constr_gen WithoutTypeConstraint
let interp_type = interp_constr_gen IsType
let open_constr_use_classes_flags () = {
- use_typeclasses = true;
+ use_typeclasses = UseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -573,7 +573,7 @@ let open_constr_use_classes_flags () = {
}
let open_constr_no_classes_flags () = {
- use_typeclasses = false;
+ use_typeclasses = NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -582,7 +582,7 @@ let open_constr_no_classes_flags () = {
}
let pure_open_constr_flags = {
- use_typeclasses = false;
+ use_typeclasses = NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = false;
diff --git a/plugins/micromega/.ocamlformat b/plugins/micromega/.ocamlformat
new file mode 100644
index 0000000000..a22a2ff88c
--- /dev/null
+++ b/plugins/micromega/.ocamlformat
@@ -0,0 +1 @@
+disable=false
diff --git a/plugins/micromega/.ocamlformat-ignore b/plugins/micromega/.ocamlformat-ignore
new file mode 100644
index 0000000000..157a987754
--- /dev/null
+++ b/plugins/micromega/.ocamlformat-ignore
@@ -0,0 +1 @@
+micromega.ml
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 01b12474dd..e0b083a70a 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -239,7 +239,7 @@ let interp_refine ist gl rc =
} in
let kind = Pretyping.OfType (pf_concl gl) in
let flags = {
- Pretyping.use_typeclasses = true;
+ Pretyping.use_typeclasses = Pretyping.UseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 10:00:51 +0000