diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comFixpoint.ml | 85 | ||||
| -rw-r--r-- | vernac/comFixpoint.mli | 51 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 6 | ||||
| -rw-r--r-- | vernac/comInductive.mli | 53 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 40 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.mli | 14 | ||||
| -rw-r--r-- | vernac/declareObl.ml | 5 | ||||
| -rw-r--r-- | vernac/declareObl.mli | 5 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 18 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 180 | ||||
| -rw-r--r-- | vernac/obligations.mli | 46 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 24 | ||||
| -rw-r--r-- | vernac/ppvernac.mli | 2 | ||||
| -rw-r--r-- | vernac/pvernac.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 18 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 23 | ||||
| -rw-r--r-- | vernac/vernacprop.ml | 1 |
17 files changed, 258 insertions, 315 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 3f13d772ab..74c9bc2886 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -107,26 +107,20 @@ let check_mutuality env evd isfix fixl = warn_non_full_mutual (x,xge,y,yge,isfix,rest) | _ -> () -type structured_fixpoint_expr = { - fix_name : Id.t; - fix_univs : universe_decl_expr option; - fix_annot : lident option; - fix_binders : local_binder_expr list; - fix_body : constr_expr option; - fix_type : constr_expr -} - let interp_fix_context ~program_mode ~cofix env sigma fix = - let before, after = if not cofix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in + let before, after = + if not cofix + then split_at_annot fix.Vernacexpr.binders fix.Vernacexpr.rec_order + else [], fix.Vernacexpr.binders in let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in let sigma, (impl_env', ((env'', ctx'), imps')) = interp_context_evars ~program_mode ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after in - let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in + let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) let interp_fix_ccl ~program_mode sigma impls (env,_) fix = - let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.fix_type in + let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.Vernacexpr.rtype in let r = Retyping.relevance_of_type env sigma c in sigma, (c, r, impl) @@ -135,7 +129,7 @@ let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl = Option.cata (fun body -> let env = push_rel_context ctx env_rec in let sigma, body = interp_casted_constr_evars ~program_mode env sigma ~impls body ccl in - sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.fix_body + sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.Vernacexpr.body_def let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx @@ -167,16 +161,16 @@ type recursive_preentry = let fix_proto sigma = Evarutil.new_global sigma (Coqlib.lib_ref "program.tactic.fix_proto") -let interp_recursive ~program_mode ~cofix fixl notations = +let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen list) = let open Context.Named.Declaration in let open EConstr in let env = Global.env() in - let fixnames = List.map (fun fix -> fix.fix_name) fixl in + let fixnames = List.map (fun fix -> fix.Vernacexpr.fname.CAst.v) fixl in (* Interp arities allowing for unresolved types *) let all_universes = List.fold_right (fun sfe acc -> - match sfe.fix_univs , acc with + match sfe.Vernacexpr.univs , acc with | None , acc -> acc | x , None -> x | Some ls , Some us -> @@ -222,6 +216,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = (* Interp bodies with rollback because temp use of notations/implicit *) let sigma, fixdefs = Metasyntax.with_syntax_protection (fun () -> + let notations = List.map_append (fun { Vernacexpr.notations } -> notations) fixl in List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations; List.fold_left4_map (fun sigma fixctximpenv -> interp_fix_body ~program_mode env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls)) @@ -248,8 +243,8 @@ let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) = let fixtypes = List.map EConstr.(to_constr evd) fixtypes in Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes) -let interp_fixpoint ~cofix l ntns = - let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l ntns in +let interp_fixpoint ~cofix l = + let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in check_recursive true env evd fix; let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) @@ -316,38 +311,29 @@ let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v | _ -> user_err Pp.(str "Well-founded induction requires Program Fixpoint or Function.") -let extract_fixpoint_components ~structonly l = - let fixl, ntnl = List.split l in - let fixl = List.map (fun (({CAst.v=id},pl),ann,bl,typ,def) -> - (* This is a special case: if there's only one binder, we pick it as the - recursive argument if none is provided. *) - let ann = Option.map (fun ann -> match bl, ann with - | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> - CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) - | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> - CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) - | _, x -> x) ann - in - let ann = Option.map (extract_decreasing_argument ~structonly) ann in - {fix_name = id; fix_annot = ann; fix_univs = pl; - fix_binders = bl; fix_body = def; fix_type = typ}) fixl in - fixl, List.flatten ntnl - -let extract_cofixpoint_components l = - let fixl, ntnl = List.split l in - List.map (fun (({CAst.v=id},pl),bl,typ,def) -> - {fix_name = id; fix_annot = None; fix_univs = pl; - fix_binders = bl; fix_body = def; fix_type = typ}) fixl, - List.flatten ntnl +(* This is a special case: if there's only one binder, we pick it as + the recursive argument if none is provided. *) +let adjust_rec_order ~structonly binders rec_order = + let rec_order = Option.map (fun rec_order -> match binders, rec_order with + | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> + CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) + | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> + CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) + | _, x -> x) rec_order + in + Option.map (extract_decreasing_argument ~structonly) rec_order let check_safe () = let open Declarations in let flags = Environ.typing_flags (Global.env ()) in flags.check_universes && flags.check_guarded -let do_fixpoint_common l = - let fixl, ntns = extract_fixpoint_components ~structonly:true l in - let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in +let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) = + let fixl = List.map (fun fix -> + Vernacexpr.{ fix + with rec_order = adjust_rec_order ~structonly:true fix.binders fix.rec_order }) fixl in + let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in + let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl in fixl, ntns, fix, List.map compute_possible_guardness_evidences info let do_fixpoint_interactive ~scope ~poly l : Lemmas.t = @@ -361,17 +347,18 @@ let do_fixpoint ~scope ~poly l = declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () -let do_cofixpoint_common l = - let fixl,ntns = extract_cofixpoint_components l in - ntns, interp_fixpoint ~cofix:true fixl ntns +let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) = + let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in + let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in + interp_fixpoint ~cofix:true fixl, ntns let do_cofixpoint_interactive ~scope ~poly l = - let ntns, cofix = do_cofixpoint_common l in + let cofix, ntns = do_cofixpoint_common l in let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); lemma let do_cofixpoint ~scope ~poly l = - let ntns, cofix = do_cofixpoint_common l in + let cofix, ntns = do_cofixpoint_common l in declare_fixpoint_generic ~scope ~poly cofix ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 982d316605..4f8e9018de 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -10,7 +10,6 @@ open Names open Constr -open Constrexpr open Vernacexpr (** {6 Fixpoints and cofixpoints} *) @@ -18,39 +17,35 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint_interactive : - scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> Lemmas.t + scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t val do_fixpoint : - scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint_interactive : - scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t + scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t val do_cofixpoint : - scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit (************************************************************************) (** Internal API *) (************************************************************************) -type structured_fixpoint_expr = { - fix_name : Id.t; - fix_univs : Constrexpr.universe_decl_expr option; - fix_annot : lident option; - fix_binders : local_binder_expr list; - fix_body : constr_expr option; - fix_type : constr_expr -} - (** Typing global fixpoints and cofixpoint_expr *) +val adjust_rec_order + : structonly:bool + -> Constrexpr.local_binder_expr list + -> Constrexpr.recursion_order_expr option + -> lident option + (** Exported for Program *) val interp_recursive : (* Misc arguments *) program_mode:bool -> cofix:bool -> (* Notations of the fixpoint / should that be folded in the previous argument? *) - structured_fixpoint_expr list -> decl_notation list -> - + lident option fix_expr_gen list -> (* env / signature / univs / evar_map *) (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * (* names / defs / types *) @@ -60,25 +55,13 @@ val interp_recursive : (** Exported for Funind *) -(** Extracting the semantical components out of the raw syntax of - (co)fixpoints declarations *) - -val extract_fixpoint_components : structonly:bool -> - (fixpoint_expr * decl_notation list) list -> - structured_fixpoint_expr list * decl_notation list +type recursive_preentry = Id.t list * Sorts.relevance list * constr option list * types list -val extract_cofixpoint_components : - (cofixpoint_expr * decl_notation list) list -> - structured_fixpoint_expr list * decl_notation list - -type recursive_preentry = - Id.t list * Sorts.relevance list * constr option list * types list - -val interp_fixpoint : - cofix:bool -> - structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * UState.universe_decl * UState.t * - (EConstr.rel_context * Impargs.manual_implicits * int option) list +val interp_fixpoint + : cofix:bool + -> lident option fix_expr_gen list + -> recursive_preentry * UState.universe_decl * UState.t * + (EConstr.rel_context * Impargs.manual_implicits * int option) list (** Very private function, do not use *) val compute_possible_guardness_evidences : diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 65db4401d9..664010c917 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -80,9 +80,6 @@ type structured_one_inductive_expr = { ind_lc : (Id.t * constr_expr) list } -type structured_inductive_expr = - local_binder_expr list * structured_one_inductive_expr list - let minductive_message = function | [] -> user_err Pp.(str "No inductive definition.") | [x] -> (Id.print x ++ str " is defined") @@ -468,9 +465,6 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not InferCumulativity.infer_inductive env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls -let interp_mutual_inductive ~template udecl (paramsl,indl) notations ~cumulative ~poly ~private_ind finite = - interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations ~cumulative ~poly ~private_ind finite - (* Very syntactical equality *) let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 97f930c0a1..285be8cd51 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -10,7 +10,6 @@ open Names open Entries -open Libnames open Vernacexpr open Constrexpr @@ -33,12 +32,20 @@ val do_mutual_inductive -> Declarations.recursivity_kind -> unit +(** User-interface API *) + +(** Prepare a "match" template for a given inductive type. + For each branch of the match, we list the constructor name + followed by enough pattern variables. + [Not_found] is raised if the given string isn't the qualid of + a known inductive type. *) + +val make_cases : Names.inductive -> string list list + (************************************************************************) -(** Internal API *) +(** Internal API, exported for Record *) (************************************************************************) -(** Exported for Record and Funind *) - (** Registering a mutual inductive definition together with its associated schemes *) @@ -55,41 +62,3 @@ val should_auto_template : Id.t -> bool -> bool (** [should_auto_template x b] is [true] when [b] is [true] and we automatically use template polymorphism. [x] is the name of the inductive under consideration. *) - -(** Exported for Funind *) - -(** Extracting the semantical components out of the raw syntax of mutual - inductive declarations *) - -type structured_one_inductive_expr = { - ind_name : Id.t; - ind_arity : constr_expr; - ind_lc : (Id.t * constr_expr) list -} - -type structured_inductive_expr = - local_binder_expr list * structured_one_inductive_expr list - -val extract_mutual_inductive_declaration_components : - (one_inductive_expr * decl_notation list) list -> - structured_inductive_expr * (*coercions:*) qualid list * decl_notation list - -(** Typing mutual inductive definitions *) -val interp_mutual_inductive - : template:bool option - -> universe_decl_expr option - -> structured_inductive_expr - -> decl_notation list - -> cumulative:bool - -> poly:bool - -> private_ind:bool - -> Declarations.recursivity_kind - -> mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list - -(** Prepare a "match" template for a given inductive type. - For each branch of the match, we list the constructor name - followed by enough pattern variables. - [Not_found] is raised if the given string isn't the qualid of - a known inductive type. *) - -val make_cases : Names.inductive -> string list list diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 0fd65ad9b4..c6e68effd7 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -244,10 +244,10 @@ let collect_evars_of_term evd c ty = Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) -let do_program_recursive ~scope ~poly fixkind fixl ntns = +let do_program_recursive ~scope ~poly fixkind fixl = let cofix = fixkind = DeclareObl.IsCoFixpoint in let (env, rec_sign, pl, evd), fix, info = - interp_recursive ~cofix ~program_mode:true fixl ntns + interp_recursive ~cofix ~program_mode:true fixl in (* Program-specific code *) (* Get the interesting evars, those that were not instantiated *) @@ -289,16 +289,19 @@ let do_program_recursive ~scope ~poly fixkind fixl ntns = | DeclareObl.IsFixpoint _ -> Decls.Fixpoint | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint in + let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind let do_program_fixpoint ~scope ~poly l = - let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in + let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in match g, l with - | [Some { CAst.v = CWfRec (n,r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> + | [Some { CAst.v = CWfRec (n,r) }], + [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] -> let recarg = mkIdentC n.CAst.v in - build_wellfounded (id, pl, bl, typ, out_def def) poly r recarg ntn + build_wellfounded (id, univs, binders, rtype, out_def body_def) poly r recarg notations - | [Some { CAst.v = CMeasureRec (n, m, r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> + | [Some { CAst.v = CMeasureRec (n, m, r) }], + [Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] -> (* We resolve here a clash between the syntax of Program Fixpoint and the one of funind *) let r = match n, r with | Some id, None -> @@ -308,25 +311,20 @@ let do_program_fixpoint ~scope ~poly l = user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.") | _, _ -> r in - build_wellfounded (id, pl, bl, typ, out_def def) poly - (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn + build_wellfounded (id, univs, binders, rtype, out_def body_def) poly + (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> - let fixl,ntns = extract_fixpoint_components ~structonly:true l in - let fixkind = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in - do_program_recursive ~scope ~poly fixkind fixl ntns + let annots = List.map (fun fix -> + Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in + let fixkind = DeclareObl.IsFixpoint annots in + let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in + do_program_recursive ~scope ~poly fixkind l | _, _ -> user_err ~hdr:"do_program_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") -let extract_cofixpoint_components l = - let fixl, ntnl = List.split l in - List.map (fun (({CAst.v=id},pl),bl,typ,def) -> - {fix_name = id; fix_annot = None; fix_univs = pl; - fix_binders = bl; fix_body = def; fix_type = typ}) fixl, - List.flatten ntnl - let check_safe () = let open Declarations in let flags = Environ.typing_flags (Global.env ()) in @@ -336,7 +334,7 @@ let do_fixpoint ~scope ~poly l = do_program_fixpoint ~scope ~poly l; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () -let do_cofixpoint ~scope ~poly l = - let fixl,ntns = extract_cofixpoint_components l in - do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl ntns; +let do_cofixpoint ~scope ~poly fixl = + let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in + do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli index f25abb95c3..a851e4dff5 100644 --- a/vernac/comProgramFixpoint.mli +++ b/vernac/comProgramFixpoint.mli @@ -1,11 +1,21 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open Vernacexpr (** Special Fixpoint handling when command is activated. *) val do_fixpoint : (* When [false], assume guarded. *) - scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint : (* When [false], assume guarded. *) - scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 0c45ff11d7..c5cbb095ca 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -29,9 +29,6 @@ type obligation = type obligations = obligation array * int -type notations = - (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list - type fixpoint_kind = | IsFixpoint of lident option list | IsCoFixpoint @@ -46,7 +43,7 @@ type program_info = ; prg_deps : Id.t list ; prg_fixkind : fixpoint_kind option ; prg_implicits : Impargs.manual_implicits - ; prg_notations : notations + ; prg_notations : Vernacexpr.decl_notation list ; prg_poly : bool ; prg_scope : DeclareDef.locality ; prg_kind : Decls.definition_object_kind diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index a8dd5040cb..2a8fa734b3 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -24,9 +24,6 @@ type obligation = type obligations = obligation array * int -type notations = - (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list - type fixpoint_kind = | IsFixpoint of lident option list | IsCoFixpoint @@ -41,7 +38,7 @@ type program_info = ; prg_deps : Id.t list ; prg_fixkind : fixpoint_kind option ; prg_implicits : Impargs.manual_implicits - ; prg_notations : notations + ; prg_notations : Vernacexpr.decl_notation list ; prg_poly : bool ; prg_scope : DeclareDef.locality ; prg_kind : Decls.definition_object_kind diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 2b475f1ef9..ad5d98669d 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -402,16 +402,19 @@ GRAMMAR EXTEND Gram ; (* (co)-fixpoints *) rec_definition: - [ [ id = ident_decl; + [ [ id_decl = ident_decl; bl = binders_fixannot; - ty = type_cstr; - def = OPT [":="; def = lconstr -> { def } ]; ntn = decl_notation -> - { let bl, annot = bl in ((id,annot,bl,ty,def),ntn) } ] ] + rtype = type_cstr; + body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation -> + { let binders, rec_order = bl in + {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations} + } ] ] ; corec_definition: - [ [ id = ident_decl; bl = binders; ty = type_cstr; - def = OPT [":="; def = lconstr -> { def }]; ntn = decl_notation -> - { ((id,bl,ty,def),ntn) } ] ] + [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr; + body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation -> + { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations} + } ]] ; type_cstr: [ [ ":"; c=lconstr -> { c } @@ -1138,7 +1141,6 @@ GRAMMAR EXTEND Gram | IDENT "Reset"; id = identref -> { VernacResetName id } | IDENT "Back" -> { VernacBack 1 } | IDENT "Back"; n = natural -> { VernacBack n } - | IDENT "BackTo"; n = natural -> { VernacBackTo n } (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index ecea9ae4c9..6a754a0cde 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -113,46 +113,6 @@ let by tac pf = (* Creating a lemma-like constant *) (************************************************************************) -(* Support for mutually proved theorems *) - -let retrieve_first_recthm uctx = function - | GlobRef.VarRef id -> - NamedDecl.get_value (Global.lookup_named id), - Decls.variable_opacity id - | GlobRef.ConstRef cst -> - let cb = Global.lookup_constant cst in - (* we get the right order somehow but surely it could be enforced in a better way *) - let uctx = UState.context uctx in - let inst = Univ.UContext.instance uctx in - let map (c, _, _) = Vars.subst_instance_constr inst c in - (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) - | _ -> assert false - -let adjust_guardness_conditions const = function - | [] -> const (* Not a recursive statement *) - | possible_indexes -> - (* Try all combinations... not optimal *) - let env = Global.env() in - let open Proof_global in - { const with proof_entry_body = - Future.chain const.proof_entry_body - (fun ((body, ctx), eff) -> - match Constr.kind body with - | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> -(* let possible_indexes = - List.map2 (fun i c -> match i with Some i -> i | None -> - List.interval 0 (List.length ((lam_assum c)))) - lemma_guard (Array.to_list fixdefs) in -*) - let env = Safe_typing.push_private_constants env eff.Evd.seff_private in - let indexes = - search_guard env - possible_indexes fixdecls in - (mkFix ((indexes,0),fixdecls), ctx), eff - | _ -> (body, ctx), eff) } - -let default_thm_id = Id.of_string "Unnamed_thm" - let check_name_freshness locality {CAst.loc;v=id} : unit = (* We check existence here: it's a bit late at Qed time *) if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || @@ -160,52 +120,6 @@ let check_name_freshness locality {CAst.loc;v=id} : unit = then user_err ?loc (Id.print id ++ str " already exists.") -let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i { Recthm.name; typ; impargs } = - let t_i = norm typ in - let kind = Decls.(IsAssumption Conjectural) in - match body with - | None -> - let open DeclareDef in - (match scope with - | Discharge -> - let impl = false in (* copy values from Vernacentries *) - let univs = match univs with - | Polymorphic_entry (_, univs) -> - (* What is going on here? *) - Univ.ContextSet.of_context univs - | Monomorphic_entry univs -> univs - in - let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in - let () = Declare.declare_variable ~name ~kind c in - (GlobRef.VarRef name,impargs) - | Global local -> - let kind = Decls.(IsAssumption Conjectural) in - let decl = Declare.ParameterEntry (None,(t_i,univs),None) in - let kn = Declare.declare_constant ~name ~local ~kind decl in - (GlobRef.ConstRef kn,impargs)) - | Some body -> - let body = norm body in - let rec body_i t = match Constr.kind t with - | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) - | CoFix (0,decls) -> mkCoFix (i,decls) - | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) - | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) - | App (t, args) -> mkApp (body_i t, args) - | _ -> - anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in - let body_i = body_i body in - let open DeclareDef in - match scope with - | Discharge -> - let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in - let c = Declare.SectionLocalDef const in - let () = Declare.declare_variable ~name ~kind c in - (GlobRef.VarRef name,impargs) - | Global local -> - let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in - let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in - (GlobRef.ConstRef kn,impargs) - let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right @@ -315,9 +229,73 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?inference_hook ?hook thms start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl (************************************************************************) -(* Commom constant saving path *) +(* Commom constant saving path, for both Qed and Admitted *) (************************************************************************) +(* Helper for process_recthms *) +let retrieve_first_recthm uctx = function + | GlobRef.VarRef id -> + NamedDecl.get_value (Global.lookup_named id), + Decls.variable_opacity id + | GlobRef.ConstRef cst -> + let cb = Global.lookup_constant cst in + (* we get the right order somehow but surely it could be enforced in a better way *) + let uctx = UState.context uctx in + let inst = Univ.UContext.instance uctx in + let map (c, _, _) = Vars.subst_instance_constr inst c in + (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) + | _ -> assert false + +(* Helper for process_recthms *) +let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Recthm.name; typ; impargs } = + let norm c = EConstr.to_constr (Evd.from_ctx uctx) c in + let body = Option.map EConstr.of_constr body in + let univs = UState.check_univ_decl ~poly uctx udecl in + let t_i = norm typ in + let kind = Decls.(IsAssumption Conjectural) in + match body with + | None -> + let open DeclareDef in + (match scope with + | Discharge -> + let impl = false in (* copy values from Vernacentries *) + let univs = match univs with + | Polymorphic_entry (_, univs) -> + (* What is going on here? *) + Univ.ContextSet.of_context univs + | Monomorphic_entry univs -> univs + in + let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in + let () = Declare.declare_variable ~name ~kind c in + GlobRef.VarRef name, impargs + | Global local -> + let kind = Decls.(IsAssumption Conjectural) in + let decl = Declare.ParameterEntry (None,(t_i,univs),None) in + let kn = Declare.declare_constant ~name ~local ~kind decl in + GlobRef.ConstRef kn, impargs) + | Some body -> + let body = norm body in + let rec body_i t = match Constr.kind t with + | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) + | CoFix (0,decls) -> mkCoFix (i,decls) + | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) + | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) + | App (t, args) -> mkApp (body_i t, args) + | _ -> + anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in + let body_i = body_i body in + let open DeclareDef in + match scope with + | Discharge -> + let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in + let c = Declare.SectionLocalDef const in + let () = Declare.declare_variable ~name ~kind c in + GlobRef.VarRef name, impargs + | Global local -> + let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in + let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in + GlobRef.ConstRef kn, impargs + (* This declares implicits and calls the hooks for all the theorems, including the main one *) let process_recthms ?fix_exn ?hook env sigma uctx ~udecl ~poly ~scope dref imps other_thms = @@ -325,10 +303,7 @@ let process_recthms ?fix_exn ?hook env sigma uctx ~udecl ~poly ~scope dref imps if List.is_empty other_thms then [] else (* there are several theorems defined mutually *) let body,opaq = retrieve_first_recthm uctx dref in - let norm c = EConstr.to_constr (Evd.from_ctx uctx) c in - let body = Option.map EConstr.of_constr body in - let uctx = UState.check_univ_decl ~poly uctx udecl in - List.map_i (save_remaining_recthms env sigma ~poly ~scope norm uctx body opaq) 1 other_thms in + List.map_i (save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq) 1 other_thms in let thms_data = (dref,imps)::other_thms_data in List.iter (fun (dref,imps) -> maybe_declare_manual_implicits false dref imps; @@ -395,10 +370,33 @@ let save_lemma_admitted ~(lemma : t) : unit = (* Saving a lemma-like constant *) (************************************************************************) +let default_thm_id = Id.of_string "Unnamed_thm" + let check_anonymity id save_ident = if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then user_err Pp.(str "This command can only be used for unnamed theorem.") +(* Support for mutually proved theorems *) + +(* Helper for finish_proved *) +let adjust_guardness_conditions const = function + | [] -> const (* Not a recursive statement *) + | possible_indexes -> + (* Try all combinations... not optimal *) + let env = Global.env() in + let open Proof_global in + { const with + proof_entry_body = + Future.chain const.proof_entry_body + (fun ((body, ctx), eff) -> + match Constr.kind body with + | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> + let env = Safe_typing.push_private_constants env eff.Evd.seff_private in + let indexes = search_guard env possible_indexes fixdecls in + (mkFix ((indexes,0),fixdecls), ctx), eff + | _ -> (body, ctx), eff) + } + let finish_proved env sigma idopt po info = let open Proof_global in let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in diff --git a/vernac/obligations.mli b/vernac/obligations.mli index f97bc784c3..2a0d0aba97 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -18,27 +18,33 @@ val check_evars : env -> evar_map -> unit val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar_info * Evar.Set.t) list -(* env, id, evars, number of function prototypes to try to clear from - evars contexts, object and type *) -val eterm_obligations : env -> Id.t -> evar_map -> int -> - ?status:Evar_kinds.obligation_definition_status -> EConstr.constr -> EConstr.types -> - (Id.t * types * Evar_kinds.t Loc.located * - (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * - unit Proofview.tactic option) array - (* Existential key, obl. name, type as product, - location of the original evar, associated tactic, - status and dependencies as indexes into the array *) - * ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) * - constr * types - (* Translations from existential identifiers to obligation identifiers - and for terms with existentials to closed terms, given a - translation from obligation identifiers to constrs, new term, new type *) - +(* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *) type obligation_info = (Id.t * types * Evar_kinds.t Loc.located * - (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array - (* ident, type, location, (opaque or transparent, expand or define), - dependencies, tactic to solve it *) + (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array + +(* env, id, evars, number of function prototypes to try to clear from + evars contexts, object and type *) +val eterm_obligations + : env + -> Id.t + -> evar_map + -> int + -> ?status:Evar_kinds.obligation_definition_status + -> EConstr.constr + -> EConstr.types + -> obligation_info * + + (* Existential key, obl. name, type as product, location of the + original evar, associated tactic, status and dependencies as + indexes into the array *) + ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) * + + (* Translations from existential identifiers to obligation + identifiers and for terms with existentials to closed terms, + given a translation from obligation identifiers to constrs, + new term, new type *) + constr * types val default_tactic : unit Proofview.tactic ref @@ -69,7 +75,7 @@ val add_mutual_definitions -> ?kind:Decls.definition_object_kind -> ?reduce:(constr -> constr) -> ?hook:DeclareDef.Hook.t -> ?opaque:bool - -> DeclareObl.notations + -> Vernacexpr.decl_notation list -> DeclareObl.fixpoint_kind -> unit val obligation diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index e676fe94db..0eb0b1b6f6 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -419,15 +419,15 @@ let string_of_theorem_kind = let open Decls in function | l -> spc() ++ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") - let pr_rec_definition ((iddecl,ro,bl,type_,def),ntn) = + let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } = let env = Global.env () in let sigma = Evd.from_env env in let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in - let annot = pr_guard_annot (pr_lconstr_expr env sigma) bl ro in - pr_ident_decl iddecl ++ pr_binders_arg bl ++ annot - ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) type_ - ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) def - ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn + let annot = pr_guard_annot (pr_lconstr_expr env sigma) binders rec_order in + pr_ident_decl (fname,univs) ++ pr_binders_arg binders ++ annot + ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) rtype + ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) body_def + ++ prlist (pr_decl_notation @@ pr_constr env sigma) notations let pr_statement head (idpl,(bl,c)) = let env = Global.env () in @@ -669,8 +669,6 @@ let string_of_definition_object_kind = let open Decls in function return ( if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i ) - | VernacBackTo i -> - return (keyword "BackTo" ++ pr_intarg i) (* State management *) | VernacWriteState s -> @@ -858,11 +856,11 @@ let string_of_definition_object_kind = let open Decls in function | DoDischarge -> keyword "Let" ++ spc () | NoDischarge -> str "" in - let pr_onecorec ((iddecl,bl,c,def),ntn) = - pr_ident_decl iddecl ++ spc() ++ pr_binders env sigma bl ++ spc() ++ str":" ++ - spc() ++ pr_lconstr_expr env sigma c ++ - pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) def ++ - prlist (pr_decl_notation @@ pr_constr env sigma) ntn + let pr_onecorec {fname; univs; binders; rtype; body_def; notations } = + pr_ident_decl (fname,univs) ++ spc() ++ pr_binders env sigma binders ++ spc() ++ str":" ++ + spc() ++ pr_lconstr_expr env sigma rtype ++ + pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) body_def ++ + prlist (pr_decl_notation @@ pr_constr env sigma) notations in return ( hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++ diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli index d4d49a09a3..9ade5afb87 100644 --- a/vernac/ppvernac.mli +++ b/vernac/ppvernac.mli @@ -14,7 +14,7 @@ val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t (** Prints a fixpoint body *) -val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t +val pr_rec_definition : Vernacexpr.fixpoint_expr -> Pp.t (** Prints a vernac expression without dot *) val pr_vernac_expr : Vernacexpr.vernac_expr -> Pp.t diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index c9eb979a90..3bd252ecef 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -23,7 +23,7 @@ module Vernac_ : val command : vernac_expr Entry.t val syntax : vernac_expr Entry.t val vernac_control : vernac_control Entry.t - val rec_definition : (fixpoint_expr * decl_notation list) Entry.t + val rec_definition : fixpoint_expr Entry.t 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/vernacentries.ml b/vernac/vernacentries.ml index 68b7462bde..9af8d8b67c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -772,7 +772,7 @@ let vernac_inductive ~atts cum lo finite indl = let vernac_fixpoint_common ~atts discharge l = if Dumpglob.dump () then - List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; + List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") l; enforce_locality_exp atts.DefAttributes.locality discharge let vernac_fixpoint_interactive ~atts discharge l = @@ -793,7 +793,7 @@ let vernac_fixpoint ~atts discharge l = let vernac_cofixpoint_common ~atts discharge l = if Dumpglob.dump () then - List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; + List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") l; enforce_locality_exp atts.DefAttributes.locality discharge let vernac_cofixpoint_interactive ~atts discharge l = @@ -963,9 +963,10 @@ let vernac_include l = (* Sections *) -let vernac_begin_section ({v=id} as lid) = +let vernac_begin_section ~poly ({v=id} as lid) = Dumpglob.dump_definition lid true "sec"; - Lib.open_section id + Lib.open_section ~poly id; + set_bool_option_value_gen ~locality:OptLocal ["Universe"; "Polymorphism"] poly let vernac_end_section {CAst.loc} = Dumpglob.dump_reference ?loc @@ -2297,7 +2298,6 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacAbort _ -> anomaly (str "type_vernac") (* Syntax *) @@ -2357,7 +2357,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacInductive (cum, priv, finite, l) -> VtDefault(fun () -> vernac_inductive ~atts cum priv finite l) | VernacFixpoint (discharge, l) -> - let opens = List.exists (fun ((_,_,_,_,p),_) -> Option.is_empty p) l in + let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in if opens then VtOpenProof (fun () -> with_def_attributes ~atts vernac_fixpoint_interactive discharge l) @@ -2365,7 +2365,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with VtDefault (fun () -> with_def_attributes ~atts vernac_fixpoint discharge l) | VernacCoFixpoint (discharge, l) -> - let opens = List.exists (fun ((_,_,_,p),_) -> Option.is_empty p) l in + let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in if opens then VtOpenProof(fun () -> with_def_attributes ~atts vernac_cofixpoint_interactive discharge l) else @@ -2396,8 +2396,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with (* Gallina extensions *) | VernacBeginSection lid -> VtNoProof(fun () -> - unsupported_attributes atts; - vernac_begin_section lid) + vernac_begin_section ~poly:(only_polymorphism atts) lid) | VernacEndSegment lid -> VtNoProof(fun () -> unsupported_attributes atts; @@ -2630,7 +2629,6 @@ and interp_expr ?proof ~atts ~st c = | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.") | VernacBack _ -> anomaly (str "VernacBack not handled by Stm.") - | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm.") (* This one is possible to handle here *) | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index ee1f839b8d..0968632c2d 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -128,18 +128,26 @@ type definition_expr = | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr * constr_expr option -type fixpoint_expr = - ident_decl * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr option +type decl_notation = lstring * constr_expr * scope_name option + +type 'a fix_expr_gen = + { fname : lident + ; univs : universe_decl_expr option + ; rec_order : 'a + ; binders : local_binder_expr list + ; rtype : constr_expr + ; body_def : constr_expr option + ; notations : decl_notation list + } -type cofixpoint_expr = - ident_decl * local_binder_expr list * constr_expr * constr_expr option +type fixpoint_expr = recursion_order_expr option fix_expr_gen +type cofixpoint_expr = unit fix_expr_gen type local_decl_expr = | AssumExpr of lname * constr_expr | DefExpr of lname * constr_expr * constr_expr option type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *) -type decl_notation = lstring * constr_expr * scope_name option type simple_binder = lident list * constr_expr type class_binder = lident * constr_expr list type 'a with_coercion = coercion_flag * 'a @@ -283,8 +291,8 @@ type nonrec vernac_expr = | VernacAssumption of (discharge * Decls.assumption_object_kind) * Declaremods.inline * (ident_decl list * constr_expr) with_coercion list | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_flag * (inductive_expr * decl_notation list) list - | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list - | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list + | VernacFixpoint of discharge * fixpoint_expr list + | VernacCoFixpoint of discharge * cofixpoint_expr list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list @@ -351,7 +359,6 @@ type nonrec vernac_expr = | VernacResetName of lident | VernacResetInitial | VernacBack of int - | VernacBackTo of int (* Commands *) | VernacCreateHintDb of string * bool diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 1dd8164ebc..747998c6cc 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -32,7 +32,6 @@ let rec has_Fail v = v |> CAst.with_val (function let is_navigation_vernac_expr = function | VernacResetInitial | VernacResetName _ - | VernacBackTo _ | VernacBack _ -> true | _ -> false |