aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml9
-rw-r--r--vernac/comTactic.ml6
-rw-r--r--vernac/comTactic.mli9
-rw-r--r--vernac/declare.ml2
-rw-r--r--vernac/egramcoq.ml4
-rw-r--r--vernac/g_vernac.mlg94
-rw-r--r--vernac/himsg.ml4
-rw-r--r--vernac/indschemes.ml2
-rw-r--r--vernac/metasyntax.ml6
-rw-r--r--vernac/pvernac.ml3
-rw-r--r--vernac/pvernac.mli2
-rw-r--r--vernac/recLemmas.ml4
12 files changed, 76 insertions, 69 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 7a7e7d6e35..f715459616 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -145,7 +145,7 @@ let build_beq_scheme_deps kn =
| Cast (x,_,_) -> aux accu (Term.applist (x,a))
| App _ -> assert false
| Ind ((kn', _), _) ->
- if MutInd.equal kn kn' then accu
+ if Environ.QMutInd.equal env kn kn' then accu
else
let eff = SchemeMutualDep (kn', !beq_scheme_kind_aux ()) in
List.fold_left aux (eff :: accu) a
@@ -253,7 +253,7 @@ let build_beq_scheme mode kn =
| Cast (x,_,_) -> aux (Term.applist (x,a))
| App _ -> assert false
| Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
- if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
+ if Environ.QMutInd.equal env kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
else begin
try
let eq = match lookup_scheme (!beq_scheme_kind_aux()) ind' with
@@ -496,7 +496,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let u,v = try destruct_ind env sigma tt1
(* trick so that the good sequence is returned*)
with e when CErrors.noncritical e -> indu,[||]
- in if eq_ind (fst u) ind
+ in if Ind.CanOrd.equal (fst u) ind
then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ]
else (
find_scheme bl_scheme_key (fst u) (*FIXME*) >>= fun c ->
@@ -539,7 +539,8 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
end
end >>= fun (sp2,i2) ->
- if not (MutInd.equal sp1 sp2) || not (Int.equal i1 i2)
+ Proofview.tclENV >>= fun env ->
+ if not (Environ.QMutInd.equal env sp1 sp2) || not (Int.equal i1 i2)
then Tacticals.New.tclZEROMSG (str "Eq should be on the same type")
else aux (Array.to_list ca1) (Array.to_list ca2)
diff --git a/vernac/comTactic.ml b/vernac/comTactic.ml
index 8a9a412362..2252d46e58 100644
--- a/vernac/comTactic.ml
+++ b/vernac/comTactic.ml
@@ -16,13 +16,13 @@ module DMap = Dyn.Map(struct type 'a t = 'a -> unit Proofview.tactic end)
let interp_map = ref DMap.empty
-type 'a tactic_interpreter = 'a Dyn.tag
-type interpretable = I : 'a tactic_interpreter * 'a -> interpretable
+type interpretable = I : 'a Dyn.tag * 'a -> interpretable
+type 'a tactic_interpreter = Interpreter of ('a -> interpretable)
let register_tactic_interpreter na f =
let t = Dyn.create na in
interp_map := DMap.add t f !interp_map;
- t
+ Interpreter (fun x -> I (t,x))
let interp_tac (I (tag,t)) =
let f = DMap.find tag !interp_map in
diff --git a/vernac/comTactic.mli b/vernac/comTactic.mli
index f1a75e1b6a..72e71d013a 100644
--- a/vernac/comTactic.mli
+++ b/vernac/comTactic.mli
@@ -9,10 +9,13 @@
(************************************************************************)
(** Tactic interpreters have to register their interpretation function *)
-type 'a tactic_interpreter
-type interpretable = I : 'a tactic_interpreter * 'a -> interpretable
+type interpretable
-(** ['a] should be marshallable if ever used with [par:] *)
+type 'a tactic_interpreter = private Interpreter of ('a -> interpretable)
+
+(** ['a] should be marshallable if ever used with [par:]. Must be
+ called no more than once per process with a particular string: make
+ sure to use partial application. *)
val register_tactic_interpreter :
string -> ('a -> unit Proofview.tactic) -> 'a tactic_interpreter
diff --git a/vernac/declare.ml b/vernac/declare.ml
index bc38ba3f6d..3a8ceb0e0f 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -162,7 +162,7 @@ let cache_constant ((sp,kn), obj) =
then Constant.make1 kn
else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(Libnames.basename sp) ++ str".")
in
- assert (Constant.equal kn' (Constant.make1 kn));
+ assert (Environ.QConstant.equal (Global.env ()) kn' (Constant.make1 kn));
Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn));
Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index b134f7b82b..123ea2c24e 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -300,13 +300,13 @@ let interp_constr_entry_key : type r. _ -> r target -> int -> r Entry.t * int op
match forpat with
| ForConstr ->
if level = 200 then Constr.binder_constr, None
- else Constr.operconstr, Some level
+ else Constr.term, Some level
| ForPattern -> Constr.pattern, Some level
let target_entry : type s. notation_entry -> s target -> s Entry.t = function
| InConstrEntry ->
(function
- | ForConstr -> Constr.operconstr
+ | ForConstr -> Constr.term
| ForPattern -> Constr.pattern)
| InCustomEntry s ->
let (entry_for_constr, entry_for_patttern) = find_custom_entry s in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index dfc7b05b51..3d6a93c888 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -48,7 +48,7 @@ let assumption_token = Entry.create "assumption_token"
let def_body = Entry.create "def_body"
let decl_notations = Entry.create "decl_notations"
let record_field = Entry.create "record_field"
-let of_type_with_opt_coercion = Entry.create "of_type_with_opt_coercion"
+let of_type = Entry.create "of_type"
let section_subset_expr = Entry.create "section_subset_expr"
let scope_delimiter = Entry.create "scope_delimiter"
let syntax_modifiers = Entry.create "syntax_modifiers"
@@ -113,10 +113,10 @@ GRAMMAR EXTEND Gram
]
;
attribute:
- [ [ k = ident ; v = attribute_value -> { Names.Id.to_string k, v } ]
+ [ [ k = ident ; v = attr_value -> { Names.Id.to_string k, v } ]
]
;
- attribute_value:
+ attr_value:
[ [ "=" ; v = string -> { VernacFlagLeaf v }
| "(" ; a = attribute_list ; ")" -> { VernacFlagList a }
| -> { VernacFlagEmpty } ]
@@ -196,8 +196,8 @@ let name_of_ident_decl : ident_decl -> name_decl =
(* Gallina declarations *)
GRAMMAR EXTEND Gram
- GLOBAL: gallina gallina_ext thm_token def_token assumption_token def_body of_type_with_opt_coercion
- record_field decl_notations rec_definition ident_decl univ_decl;
+ GLOBAL: gallina gallina_ext thm_token def_token assumption_token def_body of_type
+ record_field decl_notations fix_definition ident_decl univ_decl;
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
@@ -219,13 +219,13 @@ GRAMMAR EXTEND Gram
(* Gallina inductive declarations *)
| f = finite_token; indl = LIST1 inductive_definition SEP "with" ->
{ VernacInductive (f, indl) }
- | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+ | "Fixpoint"; recs = LIST1 fix_definition SEP "with" ->
{ VernacFixpoint (NoDischarge, recs) }
- | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+ | IDENT "Let"; "Fixpoint"; recs = LIST1 fix_definition SEP "with" ->
{ VernacFixpoint (DoDischarge, recs) }
- | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
+ | "CoFixpoint"; corecs = LIST1 cofix_definition SEP "with" ->
{ VernacCoFixpoint (NoDischarge, corecs) }
- | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
+ | IDENT "Let"; "CoFixpoint"; corecs = LIST1 cofix_definition SEP "with" ->
{ VernacCoFixpoint (DoDischarge, corecs) }
| IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l }
| IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
@@ -339,7 +339,7 @@ GRAMMAR EXTEND Gram
;
(* Inductives and records *)
opt_constructors_or_fields:
- [ [ ":="; lc = constructor_list_or_record_decl -> { lc }
+ [ [ ":="; lc = constructors_or_record -> { lc }
| -> { RecordDecl (None, []) } ] ]
;
inductive_definition:
@@ -349,7 +349,7 @@ GRAMMAR EXTEND Gram
lc=opt_constructors_or_fields; ntn = decl_notations ->
{ (((oc,id),(indpar,extrapar),c,lc),ntn) } ] ]
;
- constructor_list_or_record_decl:
+ constructors_or_record:
[ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l }
| id = identref ; c = constructor_type; "|"; l = LIST1 constructor SEP "|" ->
{ Constructors ((c id)::l) }
@@ -369,7 +369,7 @@ GRAMMAR EXTEND Gram
| -> { false } ] ]
;
(* (co)-fixpoints *)
- rec_definition:
+ fix_definition:
[ [ id_decl = ident_decl;
bl = binders_fixannot;
rtype = type_cstr;
@@ -378,7 +378,7 @@ GRAMMAR EXTEND Gram
{fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations}
} ] ]
;
- corec_definition:
+ cofix_definition:
[ [ id_decl = ident_decl; binders = binders; rtype = type_cstr;
body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notations ->
{ {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations}
@@ -427,10 +427,10 @@ GRAMMAR EXTEND Gram
| -> { [] }
] ]
;
- record_binder_body:
- [ [ l = binders; oc = of_type_with_opt_coercion;
+ field_body:
+ [ [ l = binders; oc = of_type;
t = lconstr -> { fun id -> (oc,AssumExpr (id,l,t)) }
- | l = binders; oc = of_type_with_opt_coercion;
+ | l = binders; oc = of_type;
t = lconstr; ":="; b = lconstr -> { fun id ->
(oc,DefExpr (id,l,b,Some t)) }
| l = binders; ":="; b = lconstr -> { fun id ->
@@ -442,22 +442,22 @@ GRAMMAR EXTEND Gram
;
record_binder:
[ [ id = name -> { (NoInstance,AssumExpr(id, [], CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) }
- | id = name; f = record_binder_body -> { f id } ] ]
+ | id = name; f = field_body -> { f id } ] ]
;
assum_list:
- [ [ bl = LIST1 assum_coe -> { bl } | b = simple_assum_coe -> { [b] } ] ]
+ [ [ bl = LIST1 assum_coe -> { bl } | b = assumpt -> { [b] } ] ]
;
assum_coe:
- [ [ "("; a = simple_assum_coe; ")" -> { a } ] ]
+ [ [ "("; a = assumpt; ")" -> { a } ] ]
;
- simple_assum_coe:
- [ [ idl = LIST1 ident_decl; oc = of_type_with_opt_coercion; c = lconstr ->
+ assumpt:
+ [ [ idl = LIST1 ident_decl; oc = of_type; c = lconstr ->
{ (oc <> NoInstance,(idl,c)) } ] ]
;
constructor_type:
[[ l = binders;
- t= [ coe = of_type_with_opt_coercion; c = lconstr ->
+ t= [ coe = of_type; c = lconstr ->
{ fun l id -> (coe <> NoInstance,(id,mkProdCN ~loc l c)) }
| ->
{ fun l id -> (false,(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous, None)))) } ]
@@ -468,7 +468,7 @@ GRAMMAR EXTEND Gram
constructor:
[ [ id = identref; c=constructor_type -> { c id } ] ]
;
- of_type_with_opt_coercion:
+ of_type:
[ [ ":>" -> { BackInstance }
| ":"; ">" -> { BackInstance }
| ":" -> { NoInstance } ] ]
@@ -687,7 +687,7 @@ GRAMMAR EXTEND Gram
{ VernacContext (List.flatten c) }
| IDENT "Instance"; namesup = instance_name; ":";
- t = operconstr LEVEL "200";
+ t = term LEVEL "200";
info = hint_info ;
props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } |
":="; c = lconstr -> { Some (false,c) } | -> { None } ] ->
@@ -707,13 +707,13 @@ GRAMMAR EXTEND Gram
(* Arguments *)
| IDENT "Arguments"; qid = smart_global;
- args = LIST0 argument_spec_block;
+ args = LIST0 arg_specs;
more_implicits = OPT
[ ","; impl = LIST1
- [ impl = LIST0 more_implicits_block -> { List.flatten impl } ]
+ [ impl = LIST0 implicits_alt -> { List.flatten impl } ]
SEP "," -> { impl }
];
- mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> { l } ] ->
+ mods = OPT [ ":"; l = LIST1 args_modifier SEP "," -> { l } ] ->
{ let mods = match mods with None -> [] | Some l -> List.flatten l in
let more_implicits = Option.default [] more_implicits in
VernacArguments (qid, List.flatten args, more_implicits, mods) }
@@ -732,7 +732,7 @@ GRAMMAR EXTEND Gram
idl = LIST1 identref -> { Some idl } ] ->
{ VernacGeneralizable gen } ] ]
;
- arguments_modifier:
+ args_modifier:
[ [ IDENT "simpl"; IDENT "nomatch" -> { [`ReductionDontExposeCase] }
| IDENT "simpl"; IDENT "never" -> { [`ReductionNeverUnfold] }
| IDENT "default"; IDENT "implicits" -> { [`DefaultImplicits] }
@@ -757,7 +757,7 @@ GRAMMAR EXTEND Gram
]
];
(* List of arguments implicit status, scope, modifiers *)
- argument_spec_block: [
+ arg_specs: [
[ item = argument_spec ->
{ let name, recarg_like, notation_scope = item in
[RealArg { name=name; recarg_like=recarg_like;
@@ -791,8 +791,8 @@ GRAMMAR EXTEND Gram
implicit_status = MaxImplicit}) items }
]
];
- (* Same as [argument_spec_block], but with only implicit status and names *)
- more_implicits_block: [
+ (* Same as [arg_specs], but with only implicit status and names *)
+ implicits_alt: [
[ name = name -> { [(name.CAst.v, Explicit)] }
| "["; items = LIST1 name; "]" ->
{ List.map (fun name -> (name.CAst.v, NonMaxImplicit)) items }
@@ -826,9 +826,9 @@ GRAMMAR EXTEND Gram
GLOBAL: command query_command class_rawexpr gallina_ext search_query search_queries;
gallina_ext:
- [ [ IDENT "Export"; "Set"; table = option_table; v = option_setting ->
+ [ [ IDENT "Export"; "Set"; table = setting_name; v = option_setting ->
{ VernacSetOption (true, table, v) }
- | IDENT "Export"; IDENT "Unset"; table = option_table ->
+ | IDENT "Export"; IDENT "Unset"; table = setting_name ->
{ VernacSetOption (true, table, OptionUnset) }
] ];
@@ -837,7 +837,7 @@ GRAMMAR EXTEND Gram
(* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
| IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":";
- t = operconstr LEVEL "200";
+ t = term LEVEL "200";
info = hint_info ->
{ VernacDeclareInstance (id, bl, t, info) }
@@ -885,12 +885,12 @@ GRAMMAR EXTEND Gram
{ VernacAddMLPath dir }
(* For acting on parameter tables *)
- | "Set"; table = option_table; v = option_setting ->
+ | "Set"; table = setting_name; v = option_setting ->
{ VernacSetOption (false, table, v) }
- | IDENT "Unset"; table = option_table ->
+ | IDENT "Unset"; table = setting_name ->
{ VernacSetOption (false, table, OptionUnset) }
- | IDENT "Print"; IDENT "Table"; table = option_table ->
+ | IDENT "Print"; IDENT "Table"; table = setting_name ->
{ VernacPrintOption table }
| IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 table_value
@@ -902,9 +902,9 @@ GRAMMAR EXTEND Gram
| IDENT "Add"; table = IDENT; v = LIST1 table_value ->
{ VernacAddOption ([table], v) }
- | IDENT "Test"; table = option_table; "for"; v = LIST1 table_value
+ | IDENT "Test"; table = setting_name; "for"; v = LIST1 table_value
-> { VernacMemOption (table, v) }
- | IDENT "Test"; table = option_table ->
+ | IDENT "Test"; table = setting_name ->
{ VernacPrintOption table }
| IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 table_value
@@ -1006,7 +1006,7 @@ GRAMMAR EXTEND Gram
[ [ id = global -> { Goptions.QualidRefValue id }
| s = STRING -> { Goptions.StringRefValue s } ] ]
;
- option_table:
+ setting_name:
[ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]]
;
ne_in_or_out_modules:
@@ -1191,10 +1191,10 @@ GRAMMAR EXTEND Gram
| s, None -> SetFormat ("text",s) end }
| x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at";
lev = level -> { SetItemLevel (x::l,None,lev) }
- | x = IDENT; "at"; lev = level; b = OPT constr_as_binder_kind ->
+ | x = IDENT; "at"; lev = level; b = OPT binder_interp ->
{ SetItemLevel ([x],b,lev) }
- | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,DefaultLevel) }
- | x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) }
+ | x = IDENT; b = binder_interp -> { SetItemLevel ([x],Some b,DefaultLevel) }
+ | x = IDENT; typ = explicit_subentry -> { SetEntryType (x,typ) }
] ]
;
syntax_modifiers:
@@ -1202,18 +1202,18 @@ GRAMMAR EXTEND Gram
| -> { [] }
] ]
;
- syntax_extension_type:
+ explicit_subentry:
[ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
| IDENT "bigint" -> { ETBigint }
| IDENT "binder" -> { ETBinder true }
| IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) }
- | IDENT "constr"; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
+ | IDENT "constr"; n = at_level_opt; b = OPT binder_interp -> { ETConstr (InConstrEntry,b,n) }
| IDENT "pattern" -> { ETPattern (false,None) }
| IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (false,Some n) }
| IDENT "strict"; IDENT "pattern" -> { ETPattern (true,None) }
| IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (true,Some n) }
| IDENT "closed"; IDENT "binder" -> { ETBinder false }
- | IDENT "custom"; x = IDENT; n = at_level_opt; b = OPT constr_as_binder_kind ->
+ | IDENT "custom"; x = IDENT; n = at_level_opt; b = OPT binder_interp ->
{ ETConstr (InCustomEntry x,b,n) }
] ]
;
@@ -1221,7 +1221,7 @@ GRAMMAR EXTEND Gram
[ [ "at"; n = level -> { n }
| -> { DefaultLevel } ] ]
;
- constr_as_binder_kind:
+ binder_interp:
[ [ "as"; IDENT "ident" -> { Notation_term.AsIdent }
| "as"; IDENT "pattern" -> { Notation_term.AsIdentOrPattern }
| "as"; IDENT "strict"; IDENT "pattern" -> { Notation_term.AsStrictPattern } ] ]
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 5f7eb78a40..bef9e29ac2 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -656,7 +656,7 @@ let explain_evar_not_found env sigma id =
let explain_wrong_case_info env (ind,u) ci =
let pi = pr_inductive env ind in
- if eq_ind ci.ci_ind ind then
+ if Ind.CanOrd.equal ci.ci_ind ind then
str "Pattern-matching expression on an object of inductive type" ++
spc () ++ pi ++ spc () ++ str "has invalid information."
else
@@ -1232,7 +1232,7 @@ let error_not_allowed_dependent_analysis env isrec i =
pr_inductive env i ++ str "."
let error_not_mutual_in_scheme env ind ind' =
- if eq_ind ind ind' then
+ if Ind.CanOrd.equal ind ind' then
str "The inductive type " ++ pr_inductive env ind ++
str " occurs twice."
else
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 356ccef06b..de72a30f18 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -405,7 +405,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
let get_common_underlying_mutual_inductive env = function
| [] -> assert false
| (id,(mind,i as ind))::l as all ->
- match List.filter (fun (_,(mind',_)) -> not (MutInd.equal mind mind')) l with
+ match List.filter (fun (_,(mind',_)) -> not (Environ.QMutInd.equal env mind mind')) l with
| (_,ind')::_ ->
raise (RecursionSchemeError (env, NotMutualInScheme (ind,ind')))
| [] ->
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8ce59c40c3..185abcf35b 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -61,15 +61,15 @@ let pr_registered_grammar name =
prlist pr_one entries
let pr_grammar = function
- | "constr" | "operconstr" | "binder_constr" ->
+ | "constr" | "term" | "binder_constr" ->
str "Entry constr is" ++ fnl () ++
pr_entry Pcoq.Constr.constr ++
str "and lconstr is" ++ fnl () ++
pr_entry Pcoq.Constr.lconstr ++
str "where binder_constr is" ++ fnl () ++
pr_entry Pcoq.Constr.binder_constr ++
- str "and operconstr is" ++ fnl () ++
- pr_entry Pcoq.Constr.operconstr
+ str "and term is" ++ fnl () ++
+ pr_entry Pcoq.Constr.term
| "pattern" ->
pr_entry Pcoq.Constr.pattern
| "vernac" ->
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index c9f68eed57..a7de34dd09 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -43,7 +43,8 @@ module Vernac_ =
let command = Entry.create "command"
let syntax = Entry.create "syntax_command"
let vernac_control = Entry.create "Vernac.vernac_control"
- let rec_definition = Entry.create "Vernac.rec_definition"
+ let fix_definition = Entry.create "Vernac.fix_definition"
+ let rec_definition = fix_definition
let red_expr = Entry.create "red_expr"
let hint_info = Entry.create "hint_info"
(* Main vernac entry *)
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 8ab4af7d48..dac6877cb3 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -25,7 +25,9 @@ module Vernac_ :
val command : vernac_expr Entry.t
val syntax : vernac_expr Entry.t
val vernac_control : vernac_control Entry.t
+ val fix_definition : fixpoint_expr Entry.t
val rec_definition : fixpoint_expr Entry.t
+ [@@deprecated "Deprecated in 8.13; use 'fix_definition' instead"]
val noedit_mode : vernac_expr Entry.t
val command_entry : vernac_expr Entry.t
val main_entry : vernac_control option Entry.t
diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml
index 534c358a3f..af72c01758 100644
--- a/vernac/recLemmas.ml
+++ b/vernac/recLemmas.ml
@@ -44,7 +44,7 @@ let find_mutually_recursive_statements sigma thms =
[] in
ind_hyps,ind_ccl) thms in
let inds_hyps,ind_ccls = List.split inds in
- let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> Names.MutInd.equal kn kn' in
+ let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> Environ.QMutInd.equal (Global.env ()) kn kn' in
(* Check if all conclusions are coinductive in the same type *)
(* (degenerated cartesian product since there is at most one coind ccl) *)
let same_indccl =
@@ -70,7 +70,7 @@ let find_mutually_recursive_statements sigma thms =
| [], _::_ ->
let () = match same_indccl with
| ind :: _ ->
- if List.distinct_f Names.ind_ord (List.map pi1 ind)
+ if List.distinct_f Names.Ind.CanOrd.compare (List.map pi1 ind)
then
Flags.if_verbose Feedback.msg_info
(Pp.strbrk
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 05:46:28 +0000