diff options
Diffstat (limited to 'vernac')
87 files changed, 1111 insertions, 1070 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 46f616c4ff..2bb4bac9a4 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index 5e63829411..ba5076ec2a 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 7213ba4829..fb308fd316 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -163,6 +163,16 @@ let program = let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global" +let option_locality = + let name = "Locality" in + attribute_of_list [ + ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal); + ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal); + ("export", single_key_parser ~name ~key:"export" Goptions.OptExport); + ] >>= function + | None -> return Goptions.OptDefault + | Some l -> return l + let ukey = "universes" let universe_polymorphism_option_name = ["Universe"; "Polymorphism"] diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 7ecb7e4fb0..51bab79938 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -47,6 +47,7 @@ val polymorphic : bool attribute val program : bool attribute val template : bool option attribute val locality : bool option attribute +val option_locality : Goptions.option_locality attribute val deprecation : Deprecation.t option attribute val canonical_field : bool attribute val canonical_instance : bool attribute diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index bdf8511cce..0c9b9c7255 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -691,10 +691,10 @@ let make_bl_scheme mode mind = let lnonparrec,lnamesparrec = (* TODO subst *) context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in - let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in let side_eff = side_effect_of_mode mode in let bl_goal = EConstr.of_constr bl_goal in - let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx bl_goal + let (ans, _, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, EConstr.EInstance.empty) lnamesparrec nparrec) in ([|ans|], ctx), eff @@ -821,10 +821,10 @@ let make_lb_scheme mode mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in - let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in let side_eff = side_effect_of_mode mode in let lb_goal = EConstr.of_constr lb_goal in - let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx lb_goal + let (ans, _, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in ([|ans|], ctx), eff @@ -997,13 +997,13 @@ let make_eq_decidability mode mind = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let u = Univ.Instance.empty in - let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let side_eff = side_effect_of_mode mode in - let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx - (EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec)) - (compute_dec_tact ind lnamesparrec nparrec) + let (ans, _, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx + ~typ:(EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec)) + (compute_dec_tact ind lnamesparrec nparrec) in ([|ans|], ctx), Evd.empty_side_effects diff --git a/vernac/auto_ind_decl.mli b/vernac/auto_ind_decl.mli index 0de8c61f59..dc2606c19f 100644 --- a/vernac/auto_ind_decl.mli +++ b/vernac/auto_ind_decl.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/canonical.ml b/vernac/canonical.ml index e41610b532..390ed62bee 100644 --- a/vernac/canonical.ml +++ b/vernac/canonical.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/canonical.mli b/vernac/canonical.mli index e4161b4f97..60dd4eb719 100644 --- a/vernac/canonical.mli +++ b/vernac/canonical.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/classes.ml b/vernac/classes.ml index 16b9e07fb2..dafd1cc5e4 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -29,7 +29,8 @@ module NamedDecl = Context.Named.Declaration (*i*) let set_typeclass_transparency c local b = - Hints.add_hints ~local [typeclasses_db] + let locality = if local then Goptions.OptLocal else Goptions.OptGlobal in + Hints.add_hints ~locality [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) let classes_transparent_state () = @@ -38,12 +39,11 @@ let classes_transparent_state () = with Not_found -> TransparentState.empty let () = - Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency; Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state -let add_instance_hint inst path local info poly = +let add_instance_hint inst path ~locality info poly = Flags.silently (fun () -> - Hints.add_hints ~local [typeclasses_db] + Hints.add_hints ~locality [typeclasses_db] (Hints.HintsResolveEntry [info, poly, false, Hints.PathHints path, inst])) () @@ -55,16 +55,16 @@ let is_local_for_hint i = add_instance_hint; don't ask hints to take discharge into account itself *) -let add_instance check inst = +let add_instance_base inst = let poly = Global.is_polymorphic inst.is_impl in - let local = is_local_for_hint inst in - add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] local + let locality = if is_local_for_hint inst then Goptions.OptLocal else Goptions.OptGlobal in + add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~locality inst.is_info poly; List.iter (fun (path, pri, c) -> let h = Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) [@ocaml.warning "-3"] in add_instance_hint h path - local pri poly) - (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) + ~locality pri poly) + (build_subclasses ~check:(not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) let mk_instance cl info glob impl = @@ -104,7 +104,7 @@ let discharge_instance (_, inst) = let is_local i = (i.is_global == None) let rebuild_instance inst = - add_instance true inst; + add_instance_base inst; inst let classify_instance inst = @@ -124,7 +124,7 @@ let instance_input : instance -> obj = let add_instance i = Lib.add_anonymous_leaf (instance_input i); - add_instance true i + add_instance_base i let warning_not_a_class = let name = "not-a-class" in @@ -312,29 +312,29 @@ let instance_hook info global imps ?hook cst = declare_instance env sigma (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant info global imps ?hook name decl poly sigma term termtype = +let declare_instance_constant info global imps ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in let sigma, entry = DeclareDef.prepare_definition - ~allow_evars:false ~poly sigma decl ~types:(Some termtype) ~body:term in + ~allow_evars:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in Declare.definition_message name; DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma); instance_hook info global imps ?hook (GlobRef.ConstRef kn) -let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst name = +let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name = let subst = List.fold_left2 (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') [] subst (snd k.cl_context) in let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in + let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma ~udecl ~types:termtype in let cst = Declare.declare_constant ~name ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); - instance_hook pri global imps (GlobRef.ConstRef cst) + instance_hook pri global impargs (GlobRef.ConstRef cst) -let declare_instance_program env sigma ~global ~poly name pri imps univdecl term termtype = +let declare_instance_program env sigma ~global ~poly name pri imps udecl term termtype = let hook { DeclareDef.Hook.S.scope; dref; _ } = let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in Impargs.declare_manual_implicits false dref imps; @@ -345,10 +345,10 @@ let declare_instance_program env sigma ~global ~poly name pri imps univdecl term in let obls, _, term, typ = Obligations.eterm_obligations env name sigma 0 term termtype in let hook = DeclareDef.Hook.make hook in - let ctx = Evd.evar_universe_context sigma in + let uctx = Evd.evar_universe_context sigma in let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in let _ : DeclareObl.progress = - Obligations.add_definition ~name ~term ~univdecl ~scope ~poly ~kind ~hook typ ctx obls + Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook typ ~uctx obls in () let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype = diff --git a/vernac/classes.mli b/vernac/classes.mli index 594df52c70..9698c14452 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index 9d43debb77..90791a0906 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli index cbc5fc15e2..e48e883036 100644 --- a/vernac/comArguments.mli +++ b/vernac/comArguments.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index d97bf6724c..dc9c8e2d3c 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -204,7 +204,7 @@ let context_insection sigma ~poly ctx = in let entry = Declare.definition_entry ~univs ~types:t b in let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge - ~kind:Decls.(IsDefinition Definition) UnivNames.empty_binders entry [] + ~kind:Decls.(IsDefinition Definition) ~ubind:UnivNames.empty_binders ~impargs:[] entry in () in @@ -277,18 +277,3 @@ let context ~poly l = if Global.sections_are_opened () then context_insection sigma ~poly ctx else context_nosection sigma ~poly ctx - -(* Deprecated *) -let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl name = -let open DeclareDef in -match scope with -| Discharge -> - let univs = match univs with - | Monomorphic_entry univs -> univs - | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs - in - let () = Declare.declare_universe_context ~poly univs in - declare_variable is_coe ~kind typ imps impl name; - GlobRef.VarRef name.CAst.v, Univ.Instance.empty -| Global local -> - declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl name diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index ae9edefcac..4b953c8869 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -50,19 +50,3 @@ val context : poly:bool -> local_binder_expr list -> unit - -(** Deprecated *) -val declare_assumption - : coercion_flag - -> poly:bool - -> scope:DeclareDef.locality - -> kind:Decls.assumption_object_kind - -> Constr.types - -> Entries.universes_entry - -> UnivNames.universe_binders - -> Impargs.manual_implicits - -> Glob_term.binding_kind - -> Declaremods.inline - -> variable CAst.t - -> GlobRef.t * Univ.Instance.t -[@@ocaml.deprecated "Use declare_variable or declare_axiom instead."] diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml index 2c582da495..c339c53a9b 100644 --- a/vernac/comCoercion.ml +++ b/vernac/comCoercion.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/comCoercion.mli b/vernac/comCoercion.mli index f98ef4fdd6..3b44bdaf8a 100644 --- a/vernac/comCoercion.mli +++ b/vernac/comCoercion.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 5b3f15a08c..ba2c1ac115 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -70,7 +70,7 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt = let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in let evd, ce = DeclareDef.prepare_definition ~allow_evars:program_mode - ~opaque:false ~poly evd udecl ~types:tyopt ~body:c in + ~opaque:false ~poly evd ~udecl ~types:tyopt ~body:c in (ce, evd, udecl, imps) @@ -79,9 +79,9 @@ let check_definition ~program_mode (ce, evd, _, imps) = check_evars_are_solved ~program_mode env evd; ce -let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_option c ctypopt = - let (ce, evd, univdecl, imps as def) = - interp_definition ~program_mode univdecl bl ~poly red_option c ctypopt +let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = + let (ce, evd, udecl, impargs as def) = + interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in if program_mode then let env = Global.env () in @@ -97,12 +97,12 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o let obls, _, c, cty = Obligations.eterm_obligations env name evd 0 c typ in - let ctx = Evd.evar_universe_context evd in + let uctx = Evd.evar_universe_context evd in ignore(Obligations.add_definition - ~name ~term:c cty ctx ~univdecl ~implicits:imps ~scope ~poly ~kind ?hook obls) + ~name ~term:c cty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls) else let ce = check_definition ~program_mode def in let uctx = Evd.evar_universe_context evd in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in let kind = Decls.IsDefinition kind in - ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data (Evd.universe_binders evd) ce imps) + ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind:(Evd.universe_binders evd) ce ~impargs) diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 01505d0733..6c6da8952e 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index b6843eab33..6580495295 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,22 +9,9 @@ (************************************************************************) open Pp -open CErrors open Util -open Constr -open Context -open Vars -open Termops -open Declare open Names -open Constrexpr -open Constrexpr_ops open Constrintern -open Pretyping -open Evarutil -open Evarconv - -module RelDecl = Context.Rel.Declaration (* 3c| Fixpoints and co-fixpoints *) @@ -99,7 +86,7 @@ let check_mutuality env evd isfix fixl = let names = List.map fst fixl in let preorder = List.map (fun (id,def) -> - (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' def) names)) + (id, List.filter (fun id' -> not (Id.equal id id') && Termops.occur_var env evd id' def) names)) fixl in let po = partial_order Id.equal preorder in match List.filter (function (_,Inr _) -> true | _ -> false) po with @@ -110,13 +97,13 @@ let check_mutuality env evd isfix fixl = let interp_fix_context ~program_mode ~cofix env sigma fix = let before, after = if not cofix - then split_at_annot fix.Vernacexpr.binders fix.Vernacexpr.rec_order + then Constrexpr_ops.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.Vernacexpr.rec_order in + let annot = Option.map (fun _ -> List.length (Termops.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 = @@ -134,8 +121,8 @@ let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl = let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx let prepare_recursive_declaration fixnames fixrs fixtypes fixdefs = - let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in - let names = List.map2 (fun id r -> make_annot (Name id) r) fixnames fixrs in + let defs = List.map (Vars.subst_vars (List.rev fixnames)) fixdefs in + let names = List.map2 (fun id r -> Context.make_annot (Name id) r) fixnames fixrs in (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) (* Jump over let-bindings. *) @@ -154,7 +141,7 @@ let compute_possible_guardness_evidences (ctx,_,recindex) = List.interval 0 (Context.Rel.nhyps ctx - 1) type recursive_preentry = - Id.t list * Sorts.relevance list * constr option list * types list + Id.t list * Sorts.relevance list * Constr.t option list * Constr.types list (* Wellfounded definition *) @@ -177,9 +164,9 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis let open UState in let lsu = ls.univdecl_instance and usu = us.univdecl_instance in if not (CList.for_all2eq (fun x y -> Id.equal x.CAst.v y.CAst.v) lsu usu) then - user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); + CErrors.user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); Some us) fixl None in - let sigma, decl = interp_univ_decl_opt env all_universes in + let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env all_universes in let sigma, (fixctxs, fiximppairs, fixannots) = on_snd List.split3 @@ List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma ~cofix) sigma fixl in @@ -188,7 +175,7 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis on_snd List.split3 @@ List.fold_left3_map (interp_fix_ccl ~program_mode) sigma fixctximpenvs fixctxs fixl in let fixtypes = List.map2 build_fix_type fixctxs fixccls in - let fixtypes = List.map (fun c -> nf_evar sigma c) fixtypes in + let fixtypes = List.map (fun c -> Evarutil.nf_evar sigma c) fixtypes in let fiximps = List.map3 (fun ctximps cclimps (_,ctx) -> ctximps@cclimps) fixctximps fixcclimps fixctxs in @@ -204,8 +191,8 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis Typing.solve_evars env sigma app with e when CErrors.noncritical e -> sigma, t in - sigma, LocalAssum (make_annot id Sorts.Relevant,fixprot) :: env' - else sigma, LocalAssum (make_annot id Sorts.Relevant,t) :: env') + sigma, LocalAssum (Context.make_annot id Sorts.Relevant,fixprot) :: env' + else sigma, LocalAssum (Context.make_annot id Sorts.Relevant,t) :: env') (sigma,[]) fixnames fixtypes in let env_rec = push_named_context rec_sign env in @@ -224,7 +211,7 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis () in (* Instantiate evars and check all are resolved *) - let sigma = solve_unif_constraints_with_heuristics env_rec sigma in + let sigma = Evarconv.solve_unif_constraints_with_heuristics env_rec sigma in let sigma = Evd.minimize_universes sigma in let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in @@ -238,7 +225,7 @@ let check_recursive isfix env evd (fixnames,_,fixdefs,_) = end let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) = - check_evars_are_solved ~program_mode:false env evd; + Pretyping.check_evars_are_solved ~program_mode:false env evd; let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in let fixtypes = List.map EConstr.(to_constr evd) fixtypes in Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes) @@ -249,72 +236,60 @@ let interp_fixpoint ~cofix l = let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) -let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns = - let fix_kind, cofix, indexes = match indexes with - | Some indexes -> Decls.Fixpoint, false, indexes - | None -> Decls.CoFixpoint, true, [] +let build_recthms ~indexes fixnames fixtypes fiximps = + let fix_kind, cofix = match indexes with + | Some indexes -> Decls.Fixpoint, false + | None -> Decls.CoFixpoint, true in let thms = - List.map3 (fun name t (ctx,impargs,_) -> - { Lemmas.Recthm.name; typ = EConstr.of_constr t - ; args = List.map RelDecl.get_name ctx; impargs}) - fixnames fixtypes fiximps in - let init_tac = - Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in + List.map3 (fun name typ (ctx,impargs,_) -> + { DeclareDef.Recthm.name; typ + ; args = List.map Context.Rel.Declaration.get_name ctx; impargs}) + fixnames fixtypes fiximps + in + fix_kind, cofix, thms + +let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns = + let fix_kind, cofix, thms = build_recthms ~indexes fixnames fixtypes fiximps in + let indexes = Option.default [] indexes in + let init_terms = Some fixdefs in let evd = Evd.from_ctx ctx in let lemma = Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl - evd (Some(cofix,indexes,init_tac)) thms None in + evd (Some(cofix,indexes,init_terms)) thms None in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; lemma -let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = - let indexes, cofix, fix_kind = - match indexes with - | Some indexes -> indexes, false, Decls.Fixpoint - | None -> [], true, Decls.CoFixpoint - in +let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns = (* We shortcut the proof process *) + let fix_kind, cofix, fixitems = build_recthms ~indexes fixnames fixtypes fiximps in let fixdefs = List.map Option.get fixdefs in - let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in - let vars, fixdecls, gidx = - if not cofix then - let env = Global.env() in - let indexes = search_guard env indexes fixdecls in - let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in - let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in - vars, fixdecls, Some indexes - else (* cofix *) - let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let vars = Vars.universes_of_constr (List.hd fixdecls) in - vars, fixdecls, None + let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in + let fix_kind = Decls.IsDefinition fix_kind in + let _ : GlobRef.t list = + DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx + ~possible_indexes:indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration + fixitems in - let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let evd = Evd.from_ctx ctx in - let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.check_univ_decl ~poly evd pl in - let pl = Evd.universe_binders evd in - let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in - let fixdecls = List.map mk_pure fixdecls in - ignore (List.map4 (fun name -> DeclareDef.declare_fix ~name ~scope ~kind:fix_kind pl ctx) - fixnames fixdecls fixtypes fiximps); - recursive_message (not cofix) gidx fixnames; - List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; () -let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with +let extract_decreasing_argument ~structonly { CAst.v = v; _ } = + let open Constrexpr in + match v with | CStructRec na -> na | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na | CMeasureRec (None,_,_) when not structonly -> - user_err Pp.(str "Decreasing argument must be specified in measure clause.") - | _ -> user_err Pp.(str - "Well-founded induction requires Program Fixpoint or Function.") + CErrors.user_err Pp.(str "Decreasing argument must be specified in measure clause.") + | _ -> + CErrors.user_err Pp.(str "Well-founded induction requires Program Fixpoint or Function.") (* 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 + let rec_order = Option.map (fun rec_order -> + let open Constrexpr in + 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 } -> diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 4f8e9018de..2ad6c03bae 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 718e62b9b7..1f1700b4d6 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 1286e4a5c3..2b9da1d4e5 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml index b66ff876d3..bcfbc049fa 100644 --- a/vernac/comPrimitive.ml +++ b/vernac/comPrimitive.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/comPrimitive.mli b/vernac/comPrimitive.mli index c0db1cc464..588eb7fdea 100644 --- a/vernac/comPrimitive.mli +++ b/vernac/comPrimitive.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 84f8578ad4..3bac0419ef 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -115,7 +115,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in Coqlib.check_required_library ["Coq";"Program";"Wf"]; let env = Global.env() in - let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in + let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars ~program_mode:true env sigma bl in let len = List.length binders_rel in let top_env = push_rel_context binders_rel env in @@ -234,7 +234,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ty = EConstr.Unsafe.to_constr ty in - let univs = Evd.check_univ_decl ~poly sigma decl in + let univs = Evd.check_univ_decl ~poly sigma udecl in (*FIXME poly? *) let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in (* FIXME: include locality *) @@ -258,9 +258,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let evars, _, evars_def, evars_typ = Obligations.eterm_obligations env recname sigma 0 def typ in - let ctx = Evd.evar_universe_context sigma in - ignore(Obligations.add_definition ~name:recname ~term:evars_def ~univdecl:decl - ~poly evars_typ ctx evars ~hook) + let uctx = Evd.evar_universe_context sigma in + ignore(Obligations.add_definition ~name:recname ~term:evars_def ~udecl + ~poly evars_typ ~uctx evars ~hook) let out_def = function | Some def -> def @@ -273,7 +273,7 @@ let collect_evars_of_term evd c ty = let do_program_recursive ~scope ~poly fixkind fixl = let cofix = fixkind = DeclareObl.IsCoFixpoint in - let (env, rec_sign, pl, evd), fix, info = + let (env, rec_sign, udecl, evd), fix, info = interp_recursive ~cofix ~program_mode:true fixl in (* Program-specific code *) @@ -311,13 +311,13 @@ let do_program_recursive ~scope ~poly fixkind fixl = ((indexes,i),fixdecls)) fixl end in - let ctx = Evd.evar_universe_context evd in + let uctx = Evd.evar_universe_context evd in let kind = match fixkind with | 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 + Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~udecl ~uctx ntns fixkind let do_fixpoint ~scope ~poly l = let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli index a851e4dff5..6851c9f69e 100644 --- a/vernac/comProgramFixpoint.mli +++ b/vernac/comProgramFixpoint.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 2b6f987fa6..fc53abdcea 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -43,40 +43,112 @@ module Hook = struct end (* Locality stuff *) -let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = +let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = let fix_exn = Declare.Internal.get_fix_exn ce in - let gr = match scope with + let should_suggest = ce.Declare.proof_entry_opaque && + Option.is_empty ce.Declare.proof_entry_secctx in + let dref = match scope with | Discharge -> - let () = - declare_variable ~name ~kind (SectionLocalDef ce) - in - Names.GlobRef.VarRef name + let () = declare_variable ~name ~kind (SectionLocalDef ce) in + if should_suggest then Proof_using.suggest_variable (Global.env ()) name; + Names.GlobRef.VarRef name | Global local -> - let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in - let gr = Names.GlobRef.ConstRef kn in - let () = DeclareUniv.declare_univ_binders gr udecl in - gr + let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in + let gr = Names.GlobRef.ConstRef kn in + if should_suggest then Proof_using.suggest_constant (Global.env ()) kn; + let () = DeclareUniv.declare_univ_binders gr ubind in + gr in - let () = maybe_declare_manual_implicits false gr imps in + let () = maybe_declare_manual_implicits false dref impargs in let () = definition_message name in begin match hook_data with | None -> () | Some (hook, uctx, obls) -> - Hook.call ~fix_exn ~hook { Hook.S.uctx; obls; scope; dref = gr } + Hook.call ~fix_exn ~hook { Hook.S.uctx; obls; scope; dref } end; - gr + dref -let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps = - let ce = definition_entry ~opaque ~types:t ~univs ~eff def in - let kind = Decls.IsDefinition kind in - declare_definition ~name ~scope ~kind ?hook_data udecl ce imps +let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = + match possible_indexes with + | Some possible_indexes -> + let env = Global.env() in + let indexes = Pretyping.search_guard env possible_indexes rec_declaration in + let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in + let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in + vars, fixdecls, Some indexes + | None -> + let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixitems in + let vars = Vars.universes_of_constr (List.hd fixdecls) in + vars, fixdecls, None + +module Recthm = struct + type t = + { name : Names.Id.t + (** Name of theorem *) + ; typ : Constr.t + (** Type of theorem *) + ; args : Names.Name.t list + (** Names to pre-introduce *) + ; impargs : Impargs.manual_implicits + (** Explicitily declared implicit arguments *) + } +end + +let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems = + let vars, fixdecls, indexes = + mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in + let ubind, univs = + (* XXX: Obligations don't do this, this seems like a bug? *) + if restrict_ucontext + then + let evd = Evd.from_ctx uctx in + let evd = Evd.restrict_universe_context evd vars in + let univs = Evd.check_univ_decl ~poly evd udecl in + Evd.universe_binders evd, univs + else + let univs = UState.univ_entry ~poly uctx in + UnivNames.empty_binders, univs + in + let csts = CList.map2 + (fun Recthm.{ name; typ; impargs } body -> + let ce = Declare.definition_entry ~opaque ~types:typ ~univs body in + declare_definition ~name ~scope ~kind ~ubind ~impargs ce) + fixitems fixdecls + in + let isfix = Option.is_empty possible_indexes in + let fixnames = List.map (fun { Recthm.name } -> name) fixitems in + Declare.recursive_message isfix indexes fixnames; + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; + csts + +let warn_let_as_axiom = + CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" + Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ + spc () ++ strbrk "declared as an axiom.") + +let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = + let local = match scope with + | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified + | Global local -> local + in + let kind = Decls.(IsAssumption Conjectural) in + let decl = Declare.ParameterEntry pe in + let kn = Declare.declare_constant ~name ~local ~kind decl in + let dref = Names.GlobRef.ConstRef kn in + let () = Impargs.maybe_declare_manual_implicits false dref impargs in + let () = Declare.assumption_message name in + let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in + let () = Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref}) in + dref + +(* Preparing proof entries *) let check_definition_evars ~allow_evars sigma = let env = Global.env () in if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma -let prepare_definition ~allow_evars ?opaque ?inline ~poly sigma udecl ~types ~body = +let prepare_definition ~allow_evars ?opaque ?inline ~poly ~udecl ~types ~body sigma = check_definition_evars ~allow_evars sigma; let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars) sigma (fun nf -> nf body, Option.map nf types) @@ -84,10 +156,10 @@ let prepare_definition ~allow_evars ?opaque ?inline ~poly sigma udecl ~types ~bo let univs = Evd.check_univ_decl ~poly sigma udecl in sigma, definition_entry ?opaque ?inline ?types ~univs body -let prepare_parameter ~allow_evars ~poly sigma udecl typ = +let prepare_parameter ~allow_evars ~poly ~udecl ~types sigma = check_definition_evars ~allow_evars sigma; let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars) - sigma (fun nf -> nf typ) + sigma (fun nf -> nf types) in let univs = Evd.check_univ_decl ~poly sigma udecl in sigma, (None(*proof using*), (typ, univs), None(*inline*)) diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 1bb6620886..1d7fd3a3bf 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -44,35 +44,65 @@ val declare_definition -> scope:locality -> kind:Decls.logical_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) - -> UnivNames.universe_binders + -> ubind:UnivNames.universe_binders + -> impargs:Impargs.manual_implicits -> Evd.side_effects Declare.proof_entry - -> Impargs.manual_implicits -> GlobRef.t -val declare_fix - : ?opaque:bool - -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) +val declare_assumption + : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> name:Id.t -> scope:locality - -> kind:Decls.definition_object_kind - -> UnivNames.universe_binders - -> Entries.universes_entry - -> Evd.side_effects Entries.proof_output - -> Constr.types - -> Impargs.manual_implicits + -> hook:Hook.t option + -> impargs:Impargs.manual_implicits + -> uctx:UState.t + -> Entries.parameter_entry -> GlobRef.t +module Recthm : sig + type t = + { name : Id.t + (** Name of theorem *) + ; typ : Constr.t + (** Type of theorem *) + ; args : Name.t list + (** Names to pre-introduce *) + ; impargs : Impargs.manual_implicits + (** Explicitily declared implicit arguments *) + } +end + +val declare_mutually_recursive + : opaque:bool + -> scope:locality + -> kind:Decls.logical_kind + -> poly:bool + -> uctx:UState.t + -> udecl:UState.universe_decl + -> ntns:Vernacexpr.decl_notation list + -> rec_declaration:Constr.rec_declaration + -> possible_indexes:int list list option + -> ?restrict_ucontext:bool + (** XXX: restrict_ucontext should be always true, this seems like a + bug in obligations, so this parameter should go away *) + -> Recthm.t list + -> Names.GlobRef.t list + val prepare_definition : allow_evars:bool -> ?opaque:bool -> ?inline:bool -> poly:bool - -> Evd.evar_map - -> UState.universe_decl + -> udecl:UState.universe_decl -> types:EConstr.t option -> body:EConstr.t + -> Evd.evar_map -> Evd.evar_map * Evd.side_effects Declare.proof_entry -val prepare_parameter : allow_evars:bool -> - poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types -> - Evd.evar_map * Entries.parameter_entry +val prepare_parameter + : allow_evars:bool + -> poly:bool + -> udecl:UState.universe_decl + -> types:EConstr.types + -> Evd.evar_map + -> Evd.evar_map * Entries.parameter_entry diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml index 7dd53564cc..2610f16d92 100644 --- a/vernac/declareInd.ml +++ b/vernac/declareInd.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli index 17647d50aa..ae649634a5 100644 --- a/vernac/declareInd.mli +++ b/vernac/declareInd.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index dcb28b898f..98a9e4b9c9 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -18,39 +18,96 @@ open Entries type 'a obligation_body = DefinedObl of 'a | TermObl of constr -type obligation = - { obl_name : Id.t - ; obl_type : types - ; obl_location : Evar_kinds.t Loc.located - ; obl_body : pconstant obligation_body option - ; obl_status : bool * Evar_kinds.obligation_definition_status - ; obl_deps : Int.Set.t - ; obl_tac : unit Proofview.tactic option } +module Obligation = struct + type t = + { obl_name : Id.t + ; obl_type : types + ; obl_location : Evar_kinds.t Loc.located + ; obl_body : pconstant obligation_body option + ; obl_status : bool * Evar_kinds.obligation_definition_status + ; obl_deps : Int.Set.t + ; obl_tac : unit Proofview.tactic option } -type obligations = obligation array * int + let set_type ~typ obl = { obl with obl_type = typ } + let set_body ~body obl = { obl with obl_body = Some body } + +end + +type obligations = + { obls : Obligation.t array + ; remaining : int } type fixpoint_kind = | IsFixpoint of lident option list | IsCoFixpoint -type program_info = - { prg_name : Id.t - ; prg_body : constr - ; prg_type : constr - ; prg_ctx : UState.t - ; prg_univdecl : UState.universe_decl - ; prg_obligations : obligations - ; prg_deps : Id.t list - ; prg_fixkind : fixpoint_kind option - ; prg_implicits : Impargs.manual_implicits - ; prg_notations : Vernacexpr.decl_notation list - ; prg_poly : bool - ; prg_scope : DeclareDef.locality - ; prg_kind : Decls.definition_object_kind - ; prg_reduce : constr -> constr - ; prg_hook : DeclareDef.Hook.t option - ; prg_opaque : bool - } +module ProgramDecl = struct + + type t = + { prg_name : Id.t + ; prg_body : constr + ; prg_type : constr + ; prg_ctx : UState.t + ; prg_univdecl : UState.universe_decl + ; prg_obligations : obligations + ; prg_deps : Id.t list + ; prg_fixkind : fixpoint_kind option + ; prg_implicits : Impargs.manual_implicits + ; prg_notations : Vernacexpr.decl_notation list + ; prg_poly : bool + ; prg_scope : DeclareDef.locality + ; prg_kind : Decls.definition_object_kind + ; prg_reduce : constr -> constr + ; prg_hook : DeclareDef.Hook.t option + ; prg_opaque : bool + } + + open Obligation + + let make ?(opaque = false) ?hook n ~udecl ~uctx ~impargs + ~poly ~scope ~kind b t deps fixkind notations obls reduce = + let obls', b = + match b with + | None -> + assert(Int.equal (Array.length obls) 0); + let n = Nameops.add_suffix n "_obligation" in + [| { obl_name = n; obl_body = None; + obl_location = Loc.tag Evar_kinds.InternalHole; obl_type = t; + obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty; + obl_tac = None } |], + mkVar n + | Some b -> + Array.mapi + (fun i (n, t, l, o, d, tac) -> + { obl_name = n ; obl_body = None; + obl_location = l; obl_type = t; obl_status = o; + obl_deps = d; obl_tac = tac }) + obls, b + in + let ctx = UState.make_flexible_nonalgebraic uctx in + { prg_name = n + ; prg_body = b + ; prg_type = reduce t + ; prg_ctx = ctx + ; prg_univdecl = udecl + ; prg_obligations = { obls = obls' ; remaining = Array.length obls' } + ; prg_deps = deps + ; prg_fixkind = fixkind + ; prg_notations = notations + ; prg_implicits = impargs + ; prg_poly = poly + ; prg_scope = scope + ; prg_kind = kind + ; prg_reduce = reduce + ; prg_hook = hook + ; prg_opaque = opaque + } + + let set_uctx ~uctx prg = {prg with prg_ctx = uctx} +end + +open Obligation +open ProgramDecl (* Saving an obligation *) @@ -120,15 +177,16 @@ let shrink_body c ty = in (ctx, b', ty', Array.of_list args) -let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] - -let add_hint local prg cst = - Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst) - (***********************************************************************) (* Saving an obligation *) (***********************************************************************) +let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] + +let add_hint local prg cst = + let locality = if local then Goptions.OptLocal else Goptions.OptExport in + Hints.add_hints ~locality [Id.to_string prg.prg_name] (unfold_entry cst) + (* true = hide obligations *) let get_hide_obligations = Goptions.declare_bool_option_and_ref @@ -193,45 +251,24 @@ let get_prg_info_map () = !from_prg let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] -let close sec = +let check_can_close sec = if not (ProgMap.is_empty !from_prg) then let keys = map_keys !from_prg in CErrors.user_err ~hdr:"Program" Pp.( str "Unsolved obligations when closing " - ++ str sec ++ str ":" ++ spc () + ++ Id.print sec ++ str ":" ++ spc () ++ prlist_with_sep spc (fun x -> Id.print x) keys ++ ( str (if Int.equal (List.length keys) 1 then " has " else " have ") ++ str "unsolved obligations" )) -let input : program_info CEphemeron.key ProgMap.t -> Libobject.obj = - let open Libobject in - declare_object - { (default_object "Program state") with - cache_function = (fun (na, pi) -> from_prg := pi) - ; load_function = (fun _ (_, pi) -> from_prg := pi) - ; discharge_function = - (fun _ -> - close "section"; - None ) - ; classify_function = - (fun _ -> - close "module"; - Dispose ) } - -let map_replace k v m = - ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) - -let progmap_remove prg = - Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg)) +let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) +let prgmap_op f = from_prg := f !from_prg +let progmap_remove prg = prgmap_op (ProgMap.remove prg.prg_name) +let progmap_add n prg = prgmap_op (ProgMap.add n prg) +let progmap_replace prg = prgmap_op (map_replace prg.prg_name prg) -let progmap_add n prg = - Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg)) - -let progmap_replace prg' = - Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg)) - -let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0 +let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0 let obligations_message rem = if rem > 0 then @@ -271,7 +308,7 @@ let rec intset_to = function | n -> Int.Set.add n (intset_to (pred n)) let obligation_substitution expand prg = - let obls, _ = prg.prg_obligations in + let obls = prg.prg_obligations.obls in let ints = intset_to (pred (Array.length obls)) in obl_substitution expand obls ints @@ -347,12 +384,12 @@ let declare_definition prg = in let ce = Declare.definition_entry ~fix_exn ~opaque ~types:typ ~univs body in let () = progmap_remove prg in - let ubinders = UState.universe_binders uctx in + let ubind = UState.universe_binders uctx in let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in DeclareDef.declare_definition - ~name:prg.prg_name ~scope:prg.prg_scope ubinders + ~name:prg.prg_name ~scope:prg.prg_scope ~ubind ~kind:Decls.(IsDefinition prg.prg_kind) ce - prg.prg_implicits ?hook_data + ~impargs:prg.prg_implicits ?hook_data let rec lam_index n t acc = match Constr.kind t with @@ -376,9 +413,6 @@ let compute_possible_guardness_evidences n fixbody fixtype = let ctx = fst (Term.decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx -let mk_proof c = - ((c, Univ.ContextSet.empty), Evd.empty_side_effects) - let declare_mutual_definition l = let len = List.length l in let first = List.hd l in @@ -402,53 +436,43 @@ let declare_mutual_definition l = (xdef :: defs, xobls @ obls)) l ([], []) in (* let fixdefs = List.map reduce_fix fixdefs in *) - let fixdefs, fixrs,fixtypes, fiximps = List.split4 defs in + let fixdefs, fixrs, fixtypes, fixitems = + List.fold_right2 (fun (d,r,typ,impargs) name (a1,a2,a3,a4) -> + d :: a1, r :: a2, typ :: a3, + DeclareDef.Recthm.{ name; typ; impargs; args = [] } :: a4 + ) defs first.prg_deps ([],[],[],[]) + in let fixkind = Option.get first.prg_fixkind in let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in let rvec = Array.of_list fixrs in let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in - let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in - let fixnames = first.prg_deps in - let opaque = first.prg_opaque in - let kind = if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint in - let indexes, fixdecls = + let rec_declaration = (Array.map2 make_annot namevec rvec, arrrec, recvec) in + let possible_indexes = match fixkind with | IsFixpoint wfl -> - let possible_indexes = - List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes - in - let indexes = - Pretyping.search_guard (Global.env ()) possible_indexes fixdecls - in - ( Some indexes - , List.map_i (fun i _ -> mk_proof (mkFix ((indexes, i), fixdecls))) 0 l - ) - | IsCoFixpoint -> - (None, List.map_i (fun i _ -> mk_proof (mkCoFix (i, fixdecls))) 0 l) + Some (List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes) + | IsCoFixpoint -> None in + (* In the future we will pack all this in a proper record *) + let poly, scope, ntns, opaque = first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque in + let kind = if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) else Decls.(IsDefinition CoFixpoint) in (* Declare the recursive definitions *) - let poly = first.prg_poly in - let scope = first.prg_scope in - let univs = UState.univ_entry ~poly first.prg_ctx in - let fix_exn = Hook.get get_fix_exn () in + let udecl = UState.default_univ_decl in let kns = - List.map4 - (fun name -> DeclareDef.declare_fix ~name ~opaque ~scope ~kind - UnivNames.empty_binders univs) - fixnames fixdecls fixtypes fiximps + DeclareDef.declare_mutually_recursive ~scope ~opaque ~kind + ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly + ~restrict_ucontext:false fixitems in - (* Declare notations *) - List.iter - (Metasyntax.add_notation_interpretation (Global.env ())) - first.prg_notations; - Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; + (* Only for the first constant *) + let fix_exn = Hook.get get_fix_exn () in let dref = List.hd kns in DeclareDef.Hook.(call ?hook:first.prg_hook ~fix_exn { S.uctx = first.prg_ctx; obls; scope; dref }); List.iter progmap_remove l; dref let update_obls prg obls rem = - let prg' = {prg with prg_obligations = (obls, rem)} in + let prg_obligations = { obls; remaining = rem } in + let prg' = {prg with prg_obligations} in progmap_replace prg'; obligations_message rem; if rem > 0 then Remain rem @@ -478,6 +502,17 @@ let dependencies obls n = obls; !res +let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto = + let obls = Array.copy obls in + let () = obls.(num) <- obl in + let prg = { prg with prg_ctx = uctx } in + let () = ignore (update_obls prg obls (pred rem)) in + if pred rem > 0 then begin + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then + ignore (auto (Some prg.prg_name) deps None) + end + type obligation_qed_info = { name : Id.t ; num : int @@ -489,7 +524,7 @@ let obligation_terminator entries uctx { name; num; auto } = | [entry] -> let env = Global.env () in let ty = entry.Declare.proof_entry_type in - let body, uctx = Declare.inline_private_constants ~univs:uctx env entry in + let body, uctx = Declare.inline_private_constants ~uctx env entry in let sigma = Evd.from_ctx uctx in Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); (* Declare the obligation ourselves and drop the hook *) @@ -498,7 +533,7 @@ let obligation_terminator entries uctx { name; num; auto } = let body = EConstr.to_constr sigma (EConstr.of_constr body) in let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in let ctx = Evd.evar_universe_context sigma in - let obls, rem = prg.prg_obligations in + let { obls; remaining=rem } = prg.prg_obligations in let obl = obls.(num) in let status = match obl.obl_status, entry.Declare.proof_entry_opaque with @@ -516,8 +551,6 @@ let obligation_terminator entries uctx { name; num; auto } = in let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in let (defined, obl) = declare_obligation prg obl body ty uctx in - let obls = Array.copy obls in - let () = obls.(num) <- obl in let prg_ctx = if prg.prg_poly then (* Polymorphic *) (* We merge the new universes and constraints of the @@ -531,15 +564,38 @@ let obligation_terminator entries uctx { name; num; auto } = if defined then UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) else ctx in - let prg = {prg with prg_ctx} in - ignore (update_obls prg obls (pred rem)); - if pred rem > 0 then - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then - ignore (auto (Some name) deps None) + update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto | _ -> CErrors.anomaly Pp.( str "[obligation_terminator] close_proof returned more than one proof \ term") + +(* Similar to the terminator but for interactive paths, as the + terminator is only called in interactive proof mode *) +let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } = + let { obls; remaining=rem } = prg.prg_obligations in + let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in + let transparent = evaluable_constant cst (Global.env ()) in + let () = match obl.obl_status with + (true, Evar_kinds.Expand) + | (true, Evar_kinds.Define true) -> + if not transparent then err_not_transp () + | _ -> () + in + let inst, ctx' = + if not prg.prg_poly (* Not polymorphic *) then + (* The universe context was declared globally, we continue + from the new global environment. *) + let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let ctx' = UState.merge_subst ctx (UState.subst ctx') in + Univ.Instance.empty, ctx' + else + (* We get the right order somehow, but surely it could be enforced in a clearer way. *) + let uctx = UState.context ctx' in + Univ.UContext.instance uctx, ctx' + in + let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in + let () = if transparent then add_hint true prg cst in + update_program_decl_on_defined prg obls num obl ~uctx:ctx' rem ~auto diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index 7d8a112cc6..16c0413caf 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,61 +13,101 @@ open Constr type 'a obligation_body = DefinedObl of 'a | TermObl of constr -type obligation = - { obl_name : Id.t - ; obl_type : types - ; obl_location : Evar_kinds.t Loc.located - ; obl_body : pconstant obligation_body option - ; obl_status : bool * Evar_kinds.obligation_definition_status - ; obl_deps : Int.Set.t - ; obl_tac : unit Proofview.tactic option } +module Obligation : sig -type obligations = obligation array * int + type t = private + { obl_name : Id.t + ; obl_type : types + ; obl_location : Evar_kinds.t Loc.located + ; obl_body : pconstant obligation_body option + ; obl_status : bool * Evar_kinds.obligation_definition_status + ; obl_deps : Int.Set.t + ; obl_tac : unit Proofview.tactic option } + + val set_type : typ:Constr.types -> t -> t + val set_body : body:pconstant obligation_body -> t -> t + +end + +type obligations = + { obls : Obligation.t array + ; remaining : int } type fixpoint_kind = | IsFixpoint of lident option list | IsCoFixpoint -type program_info = - { prg_name : Id.t - ; prg_body : constr - ; prg_type : constr - ; prg_ctx : UState.t - ; prg_univdecl : UState.universe_decl - ; prg_obligations : obligations - ; prg_deps : Id.t list - ; prg_fixkind : fixpoint_kind option - ; prg_implicits : Impargs.manual_implicits - ; prg_notations : Vernacexpr.decl_notation list - ; prg_poly : bool - ; prg_scope : DeclareDef.locality - ; prg_kind : Decls.definition_object_kind - ; prg_reduce : constr -> constr - ; prg_hook : DeclareDef.Hook.t option - ; prg_opaque : bool - } +(* Information about a single [Program {Definition,Lemma,..}] declaration *) +module ProgramDecl : sig + + type t = private + { prg_name : Id.t + ; prg_body : constr + ; prg_type : constr + ; prg_ctx : UState.t + ; prg_univdecl : UState.universe_decl + ; prg_obligations : obligations + ; prg_deps : Id.t list + ; prg_fixkind : fixpoint_kind option + ; prg_implicits : Impargs.manual_implicits + ; prg_notations : Vernacexpr.decl_notation list + ; prg_poly : bool + ; prg_scope : DeclareDef.locality + ; prg_kind : Decls.definition_object_kind + ; prg_reduce : constr -> constr + ; prg_hook : DeclareDef.Hook.t option + ; prg_opaque : bool + } + + val make : + ?opaque:bool + -> ?hook:DeclareDef.Hook.t + -> Names.Id.t + -> udecl:UState.universe_decl + -> uctx:UState.t + -> impargs:Impargs.manual_implicits + -> poly:bool + -> scope:DeclareDef.locality + -> kind:Decls.definition_object_kind + -> Constr.constr option + -> Constr.types + -> Names.Id.t list + -> fixpoint_kind option + -> Vernacexpr.decl_notation list + -> ( Names.Id.t + * Constr.types + * Evar_kinds.t Loc.located + * (bool * Evar_kinds.obligation_definition_status) + * Int.Set.t + * unit Proofview.tactic option ) + array + -> (Constr.constr -> Constr.constr) + -> t + + val set_uctx : uctx:UState.t -> t -> t +end val declare_obligation : - program_info - -> obligation + ProgramDecl.t + -> Obligation.t -> Constr.types -> Constr.types option -> Entries.universes_entry - -> bool * obligation + -> bool * Obligation.t (** [declare_obligation] Save an obligation *) module ProgMap : CMap.ExtS with type key = Id.t and module Set := Id.Set -val declare_definition : program_info -> Names.GlobRef.t +val declare_definition : ProgramDecl.t -> Names.GlobRef.t +(** Resolution status of a program *) type progress = - (* Resolution status of a program *) | Remain of int - (* n obligations remaining *) + (** n obligations remaining *) | Dependent - (* Dependent on other definitions *) + (** Dependent on other definitions *) | Defined of GlobRef.t - (* Defined as id *) + (** Defined as id *) type obligation_qed_info = { name : Id.t @@ -79,32 +119,44 @@ val obligation_terminator : Evd.side_effects Declare.proof_entry list -> UState.t -> obligation_qed_info -> unit -(** [obligation_terminator] part 2 of saving an obligation *) +(** [obligation_terminator] part 2 of saving an obligation, proof mode *) + +val obligation_hook + : ProgramDecl.t + -> Obligation.t + -> Int.t + -> (Names.Id.t option -> Int.Set.t -> 'a option -> 'b) + -> DeclareDef.Hook.S.t + -> unit +(** [obligation_hook] part 2 of saving an obligation, non-interactive mode *) val update_obls : - program_info - -> obligation array + ProgramDecl.t + -> Obligation.t array -> int -> progress (** [update_obls prg obls n progress] What does this do? *) (** { 2 Util } *) -val get_prg_info_map : unit -> program_info CEphemeron.key ProgMap.t +(** Check obligations are properly solved before closing a section *) +val check_can_close : Id.t -> unit + +val get_prg_info_map : unit -> ProgramDecl.t CEphemeron.key ProgMap.t val program_tcc_summary_tag : - program_info CEphemeron.key Id.Map.t Summary.Dyn.tag + ProgramDecl.t CEphemeron.key Id.Map.t Summary.Dyn.tag val obl_substitution : bool - -> obligation array + -> Obligation.t array -> Int.Set.t -> (ProgMap.key * (Constr.types * Constr.types)) list -val dependencies : obligation array -> int -> Int.Set.t +val dependencies : Obligation.t array -> int -> Int.Set.t val err_not_transp : unit -> unit -val progmap_add : ProgMap.key -> program_info CEphemeron.key -> unit +val progmap_add : ProgMap.key -> ProgramDecl.t CEphemeron.key -> unit (* This is a hack to make it possible for Obligations to craft a Qed * behind the scenes. The fix_exn the Stm attaches to the Future proof diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml index def2fdad2a..300dfe6c35 100644 --- a/vernac/declareUniv.ml +++ b/vernac/declareUniv.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli index ce2a6e225c..51f3f5e0fb 100644 --- a/vernac/declareUniv.mli +++ b/vernac/declareUniv.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index e645fc552b..4f527b73d0 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli index 23f25bc597..e37299aad6 100644 --- a/vernac/declaremods.mli +++ b/vernac/declaremods.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index ead86bd12f..5dae389a62 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -368,7 +368,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = | TTClosedBinderList tkl -> MayRecNo (Alist1sep (Aentry Constr.binder, make_sep_rules tkl)) | TTName -> MayRecNo (Aentry Prim.name) | TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders) -| TTBigint -> MayRecNo (Aentry Prim.bigint) +| TTBigint -> MayRecNo (Aentry Prim.bignat) | TTReference -> MayRecNo (Aentry Constr.global) let interp_entry forpat e = match e with @@ -411,8 +411,8 @@ match e with | TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists } | TTBigint -> begin match forpat with - | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,NumTok.int v))) - | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,NumTok.int v))) + | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (NumTok.Signed.of_int_string v))) + | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (NumTok.Signed.of_int_string v))) end | TTReference -> begin match forpat with diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli index 6768d24d5c..9dc60b3b0c 100644 --- a/vernac/egramcoq.mli +++ b/vernac/egramcoq.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/egramml.ml b/vernac/egramml.ml index 2b1d99c7a9..793aad6b24 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/egramml.mli b/vernac/egramml.mli index 1fe2395df2..7f6656b079 100644 --- a/vernac/egramml.mli +++ b/vernac/egramml.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 03dfc576a1..247f80181a 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index c1414c552a..a8f1a49086 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -107,35 +107,40 @@ GRAMMAR EXTEND Gram | -> { VernacFlagEmpty } ] ] ; - vernac: - [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in (("local", VernacFlagEmpty) :: f, v) } - | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in (("global", VernacFlagEmpty) :: f, v) } - - | v = vernac_poly -> { v } ] - ] + legacy_attr: + [ [ IDENT "Local" -> + { ("local", VernacFlagEmpty) } + | IDENT "Global" -> + { ("global", VernacFlagEmpty) } + | IDENT "Polymorphic" -> + { Attributes.vernac_polymorphic_flag } + | IDENT "Monomorphic" -> + { Attributes.vernac_monomorphic_flag } + | IDENT "Cumulative" -> + { ("universes", VernacFlagList ["cumulative", VernacFlagEmpty]) } + | IDENT "NonCumulative" -> + { ("universes", VernacFlagList ["noncumulative", VernacFlagEmpty]) } + | IDENT "Private" -> + { ("private", VernacFlagList ["matching", VernacFlagEmpty]) } + | IDENT "Program" -> + { ("program", VernacFlagEmpty) } + ] ] ; - vernac_poly: - [ [ IDENT "Polymorphic"; v = vernac_aux -> - { let (f, v) = v in (Attributes.vernac_polymorphic_flag :: f, v) } - | IDENT "Monomorphic"; v = vernac_aux -> - { let (f, v) = v in (Attributes.vernac_monomorphic_flag :: f, v) } - | v = vernac_aux -> { v } ] - ] + vernac: + [ [ attrs = LIST0 legacy_attr; v = vernac_aux -> { (attrs, v) } ] ] ; vernac_aux: (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *) (* "." is still in the stream and discard_to_dot works correctly *) - [ [ IDENT "Program"; g = gallina; "." -> { (["program", VernacFlagEmpty], g) } - | IDENT "Program"; g = gallina_ext; "." -> { (["program", VernacFlagEmpty], g) } - | g = gallina; "." -> { ([], g) } - | g = gallina_ext; "." -> { ([], g) } - | c = command; "." -> { ([], c) } - | c = syntax; "." -> { ([], c) } - | c = subprf -> { ([], c) } + [ [ g = gallina; "." -> { g } + | g = gallina_ext; "." -> { g } + | c = command; "." -> { c } + | c = syntax; "." -> { c } + | c = subprf -> { c } ] ] ; vernac_aux: LAST - [ [ prfcom = command_entry -> { ([], prfcom) } ] ] + [ [ prfcom = command_entry -> { prfcom } ] ] ; noedit_mode: [ [ c = query_command -> { c None } ] ] @@ -197,9 +202,8 @@ GRAMMAR EXTEND Gram | IDENT "Let"; id = identref; b = def_body -> { VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b) } (* Gallina inductive declarations *) - | cum = OPT cumulativity_token; priv = private_token; f = finite_token; - indl = LIST1 inductive_definition SEP "with" -> - { VernacInductive (cum, priv, f, indl) } + | f = finite_token; indl = LIST1 inductive_definition SEP "with" -> + { VernacInductive (f, indl) } | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> { VernacFixpoint (NoDischarge, recs) } | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> @@ -341,13 +345,6 @@ GRAMMAR EXTEND Gram | IDENT "Structure" -> { Structure } | IDENT "Class" -> { Class true } ] ] ; - cumulativity_token: - [ [ IDENT "Cumulative" -> { VernacCumulative } - | IDENT "NonCumulative" -> { VernacNonCumulative } ] ] - ; - private_token: - [ [ IDENT "Private" -> { true } | -> { false } ] ] - ; (* Simple definitions *) def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> @@ -986,13 +983,6 @@ GRAMMAR EXTEND Gram { fun g -> VernacSearch (SearchRewrite c,g, l) } | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> { let (sl,m) = l in fun g -> VernacSearch (Search (s::sl),g, m) } - (* compatibility: SearchAbout *) - | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." -> - { fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) } - (* compatibility: SearchAbout with "[ ... ]" *) - | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]"; - l = in_or_out_modules; "." -> - { fun g -> VernacSearch (SearchAbout sl,g, l) } ] ] ; printable: diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 07ec6ca1ba..5555a2c68e 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/himsg.mli b/vernac/himsg.mli index 9de5284393..f0aa50f227 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 80616ecc2a..7260b13ff6 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli index a747ac6598..16e3bcfb7c 100644 --- a/vernac/indschemes.mli +++ b/vernac/indschemes.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 68f4f55d0e..e08d2ce117 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,15 +11,8 @@ (* Created by Hugo Herbelin from contents related to lemma proofs in file command.ml, Aug 2009 *) -open CErrors open Util -open Pp open Names -open Constr -open Declareops -open Nameops -open Pretyping -open Impargs module NamedDecl = Context.Named.Declaration @@ -46,15 +39,6 @@ module Proof_ending = struct end -module Recthm = struct - type t = - { name : Id.t - ; typ : EConstr.t - ; args : Name.t list - ; impargs : Impargs.manual_implicits - } -end - module Info = struct type t = @@ -63,7 +47,7 @@ module Info = struct ; impargs : Impargs.manual_implicits ; proof_ending : Proof_ending.t CEphemeron.key (* This could be improved and the CEphemeron removed *) - ; other_thms : Recthm.t list + ; other_thms : DeclareDef.Recthm.t list ; scope : DeclareDef.locality ; kind : Decls.logical_kind } @@ -136,7 +120,7 @@ let start_dependent_lemma ~name ~poly let rec_tac_initializer finite guard thms snl = if finite then - match List.map (fun { Recthm.name; typ } -> name,typ) thms with + match List.map (fun { DeclareDef.Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else @@ -144,28 +128,32 @@ let rec_tac_initializer finite guard thms snl = let nl = match snl with | None -> List.map succ (List.map List.last guard) | Some nl -> nl - in match List.map2 (fun { Recthm.name; typ } n -> (name, n, typ)) thms nl with + in match List.map2 (fun { DeclareDef.Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl = - let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in + let intro_tac { DeclareDef.Recthm.args; _ } = Tactics.auto_intros_tac args in let init_tac, compute_guard = match recguard with - | Some (finite,guard,init_tac) -> + | Some (finite,guard,init_terms) -> let rec_tac = rec_tac_initializer finite guard thms snl in - Some (match init_tac with - | None -> - Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms) - | Some tacl -> - Tacticals.New.tclTHENS rec_tac - List.(map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms) - ),guard + let term_tac = + match init_terms with + | None -> + List.map intro_tac thms + | Some init_terms -> + (* This is the case for hybrid proof mode / definition + fixpoint, where terms for some constants are given with := *) + let tacl = List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) init_terms in + List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms + in + Tacticals.New.tclTHENS rec_tac term_tac, guard | None -> let () = match thms with [_] -> () | _ -> assert false in - Some (intro_tac (List.hd thms)), [] in + intro_tac (List.hd thms), [] in match thms with - | [] -> anomaly (Pp.str "No proof to start.") - | { Recthm.name; typ; impargs; _}::other_thms -> + | [] -> CErrors.anomaly (Pp.str "No proof to start.") + | { DeclareDef.Recthm.name; typ; impargs; _}::other_thms -> let info = Info.{ hook ; impargs @@ -175,142 +163,178 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua ; scope ; kind } in - let lemma = start_lemma ~name ~poly ~udecl ~info sigma typ in + let lemma = start_lemma ~name ~poly ~udecl ~info sigma (EConstr.of_constr typ) in pf_map (Proof_global.map_proof (fun p -> - match init_tac with - | None -> p - | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma + pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)) lemma (************************************************************************) (* 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 Fixpoint + Admitted gets turned into axiom so scope is Global, - see finish_admitted *) - assert false - | 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 = - let other_thms_data = - if List.is_empty other_thms then [] else - (* there are several theorems defined mutually *) - let body,opaq = retrieve_first_recthm uctx dref 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; - DeclareDef.Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref})) thms_data +(* Support for mutually proved theorems *) + +(* XXX: Most of this does belong to Declare, due to proof_entry manip *) +module MutualEntry : sig + + val declare_variable + : info:Info.t + -> uctx:UState.t + (* Only for the first constant, introduced by compat *) + -> ubind:UnivNames.universe_binders + -> name:Id.t + -> Entries.parameter_entry + -> Names.GlobRef.t list + + val declare_mutdef + (* Common to all recthms *) + : info:Info.t + -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) + -> uctx:UState.t + -> ?hook_data:DeclareDef.Hook.t * UState.t * (Names.Id.t * Constr.t) list + (* Only for the first constant, introduced by compat *) + -> ubind:UnivNames.universe_binders + -> name:Id.t + -> Evd.side_effects Declare.proof_entry + -> Names.GlobRef.t list + +end = struct + + (* Body with the fix *) + type et = + | NoBody of Entries.parameter_entry + | Single of Evd.side_effects Declare.proof_entry + | Mutual of Evd.side_effects Declare.proof_entry + + type t = + { entry : et + ; info : Info.t + } + + (* XXX: Refactor this with the code in + [ComFixpoint.declare_fixpoint_generic] *) + let guess_decreasing env possible_indexes ((body, ctx), eff) = + let open Constr in + 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 = Pretyping.search_guard env possible_indexes fixdecls in + (mkFix ((indexes,0),fixdecls), ctx), eff + | _ -> (body, ctx), eff + + let adjust_guardness_conditions ~info const = + let entry = match info.Info.compute_guard with + | [] -> + (* Not a recursive statement *) + Single const + | possible_indexes -> + (* Try all combinations... not optimal *) + let env = Global.env() in + let pe = Declare.Internal.map_entry_body const + ~f:(guess_decreasing env possible_indexes) + in + Mutual pe + in { entry; info } + + let rec select_body i t = + let open Constr in + 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, select_body i t2) + | Lambda(na,ty,t) -> mkLambda(na,ty, select_body i t) + | App (t, args) -> mkApp (select_body i t, args) + | _ -> + CErrors.anomaly + Pp.(str "Not a proof by induction: " ++ + Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".") + + let declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name ?typ ~impargs ~info mutpe i = + let { Info.hook; compute_guard; scope; kind; _ } = info in + match mutpe with + | NoBody pe -> + DeclareDef.declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe + | Single pe -> + (* We'd like to do [assert (i = 0)] here, however this codepath + is used when declaring mutual cofixpoints *) + DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe + | Mutual pe -> + (* if typ = None , we don't touch the type; used in the base case *) + let pe = + match typ with + | None -> pe + | Some typ -> + Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ) + in + let pe = Declare.Internal.map_entry_body pe + ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in + DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe + + let declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name { entry; info } = + (* At some point make this a single iteration *) + (* At some point make this a single iteration *) + (* impargs here are special too, fixed in upcoming PRs *) + let impargs = info.Info.impargs in + let r = declare_mutdef ?fix_exn ~info ~ubind ?hook_data ~uctx ~name ~impargs entry 0 in + (* Before we used to do this, check if that's right *) + let ubind = UnivNames.empty_binders in + let rs = + List.map_i ( + fun i { DeclareDef.Recthm.name; typ; impargs } -> + declare_mutdef ?fix_exn ~name ~info ~ubind ?hook_data ~uctx ~typ ~impargs entry i) 1 info.Info.other_thms + in r :: rs + + let declare_variable ~info ~uctx ~ubind ~name pe = + declare_mutdef ~uctx ~ubind ~name { entry = NoBody pe; info } + + let declare_mutdef ~info ?fix_exn ~uctx ?hook_data ~ubind ~name const = + let mutpe = adjust_guardness_conditions ~info const in + declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name mutpe + +end (************************************************************************) (* Admitting a lemma-like constant *) (************************************************************************) (* Admitted *) -let warn_let_as_axiom = - CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" - (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++ - spc () ++ strbrk "declared as an axiom.") - let get_keep_admitted_vars = Goptions.declare_bool_option_and_ref ~depr:false ~key:["Keep"; "Admitted"; "Variables"] ~value:true -let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs other_thms = - let open DeclareDef in - let local = match scope with - | Global local -> local - | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified - in - let kn = Declare.declare_constant ~name ~local ~kind:Decls.(IsAssumption Conjectural) (Declare.ParameterEntry pe) in - let () = Declare.assumption_message name in - DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx); - (* This takes care of the implicits and hook for the current constant*) - process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms +let compute_proof_using_for_admitted proof typ pproofs = + if not (get_keep_admitted_vars ()) then None + else match Proof_global.get_used_variables proof, pproofs with + | Some _ as x, _ -> x + | None, pproof :: _ -> + let env = Global.env () in + let ids_typ = Environ.global_vars_set env typ in + (* [pproof] is evar-normalized by [partial_proof]. We don't + count variables appearing only in the type of evars. *) + let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in + Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) + | _ -> None + +let finish_admitted ~name ~info ~uctx pe = + let ubind = UnivNames.empty_binders in + let _r : Names.GlobRef.t list = MutualEntry.declare_variable ~info ~uctx ~ubind ~name pe in + () let save_lemma_admitted ~(lemma : t) : unit = - (* Used for printing in recthms *) - let env = Global.env () in - let { Info.hook; scope; impargs; other_thms } = lemma.info in let udecl = Proof_global.get_universe_decl lemma.proof in - let Proof.{ sigma; name; poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in + let Proof.{ name; poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in let typ = match Proofview.initial_goals entry with | [typ] -> snd typ - | _ -> CErrors.anomaly ~label:"Lemmas.save_proof" (Pp.str "more than one statement.") + | _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.") in let typ = EConstr.Unsafe.to_constr typ in let proof = Proof_global.get_proof lemma.proof in let pproofs = Proof.partial_proof proof in - let sec_vars = - if not (get_keep_admitted_vars ()) then None - else match Proof_global.get_used_variables lemma.proof, pproofs with - | Some _ as x, _ -> x - | None, pproof :: _ -> - let env = Global.env () in - let ids_typ = Environ.global_vars_set env typ in - (* [pproof] is evar-normalized by [partial_proof]. We don't - count variables appearing only in the type of evars. *) - let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in - Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) - | _ -> None in + let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in let universes = Proof_global.get_initial_euctx lemma.proof in let ctx = UState.check_univ_decl ~poly universes udecl in - finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms + finish_admitted ~name ~info:lemma.info ~uctx:universes (sec_vars, (typ, ctx), None) (************************************************************************) (* Saving a lemma-like constant *) @@ -319,67 +343,30 @@ let save_lemma_admitted ~(lemma : t) : unit = 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 *) + if not (String.equal (Nameops.atompart_of_id id) (Id.to_string (default_thm_id))) then + CErrors.user_err Pp.(str "This command can only be used for unnamed theorem.") -(* 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 - Declare.Internal.map_entry_body const - ~f:(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 finish_proved idopt po info = let open Proof_global in - let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in + let { Info.hook } = info in match po with - | { name; entries=[const]; universes; udecl; poly } -> + | { name; entries=[const]; uctx; udecl } -> let name = match idopt with | None -> name | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in let fix_exn = Declare.Internal.get_fix_exn const in let () = try - let const = adjust_guardness_conditions const compute_guard in - let should_suggest = const.Declare.proof_entry_opaque && - Option.is_empty const.Declare.proof_entry_secctx in - let open DeclareDef in - let r = match scope with - | Discharge -> - let c = Declare.SectionLocalDef const in - let () = Declare.declare_variable ~name ~kind c in - let () = if should_suggest - then Proof_using.suggest_variable (Global.env ()) name - in - GlobRef.VarRef name - | Global local -> - let kn = - Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in - let () = if should_suggest - then Proof_using.suggest_constant (Global.env ()) kn - in - let gr = GlobRef.ConstRef kn in - DeclareUniv.declare_univ_binders gr (UState.universe_binders universes); - gr - in - Declare.definition_message name; - (* This takes care of the implicits and hook for the current constant*) - process_recthms ~fix_exn ?hook env sigma universes ~udecl ~poly ~scope r impargs other_thms + let hook_data = Option.map (fun hook -> hook, uctx, []) hook in + let ubind = UState.universe_binders uctx in + let _r : Names.GlobRef.t list = + MutualEntry.declare_mutdef ~info ~fix_exn ~uctx ?hook_data ~ubind ~name const + in () with e when CErrors.noncritical e -> let e = Exninfo.capture e in Exninfo.iraise (fix_exn e) in () | _ -> - CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term") + CErrors.anomaly ~label:"finish_proved" Pp.(str "close_proof returned more than one proof term") let finish_derived ~f ~name ~idopt ~entries = (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *) @@ -399,7 +386,7 @@ let finish_derived ~f ~name ~idopt ~entries = let f_kind = Decls.(IsDefinition Definition) in let f_def = Declare.DefinitionEntry f_def in let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in - let f_kn_term = mkConst f_kn in + let f_kn_term = Constr.mkConst f_kn in (* In the type and body of the proof of [suchthat] there can be references to the variable [f]. It needs to be replaced by references to the constant [f] declared above. This substitution @@ -427,7 +414,7 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = let id = match Evd.evar_ident ev sigma0 with | Some id -> id - | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n) + | None -> let n = !obls in incr obls; Nameops.add_suffix i ("_obligation_" ^ string_of_int n) in let entry, args = Declare.Internal.shrink_entry local_context entry in let cst = Declare.declare_constant ~name:id ~kind (Declare.DefinitionEntry entry) in @@ -438,14 +425,14 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = in hook recobls sigma -let finalize_proof idopt env sigma proof_obj proof_info = +let finalize_proof idopt proof_obj proof_info = let open Proof_global in let open Proof_ending in match CEphemeron.default proof_info.Info.proof_ending Regular with | Regular -> - finish_proved env sigma idopt proof_obj proof_info + finish_proved idopt proof_obj proof_info | End_obligation oinfo -> - DeclareObl.obligation_terminator proof_obj.entries proof_obj.universes oinfo + DeclareObl.obligation_terminator proof_obj.entries proof_obj.uctx oinfo | End_derive { f ; name } -> finish_derived ~f ~name ~idopt ~entries:proof_obj.entries | End_equations { hook; i; types; wits; sigma } -> @@ -453,35 +440,26 @@ let finalize_proof idopt env sigma proof_obj proof_info = let save_lemma_proved ~lemma ~opaque ~idopt = (* Env and sigma are just used for error printing in save_remaining_recthms *) - let env = Global.env () in - let { Proof.sigma } = Proof.data (Proof_global.get_proof lemma.proof) in let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) lemma.proof in - finalize_proof idopt env sigma proof_obj lemma.info + finalize_proof idopt proof_obj lemma.info (***********************************************************************) (* Special case to close a lemma without forcing a proof *) (***********************************************************************) let save_lemma_admitted_delayed ~proof ~info = let open Proof_global in - let env = Global.env () in - let sigma = Evd.from_env env in - let { name; entries; universes; udecl; poly } = proof in - let { Info.hook; scope; impargs; other_thms } = info in + let { name; entries; uctx; udecl } = proof in if List.length entries <> 1 then - user_err Pp.(str "Admitted does not support multiple statements"); + CErrors.user_err Pp.(str "Admitted does not support multiple statements"); let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in let poly = match proof_entry_universes with | Entries.Monomorphic_entry _ -> false | Entries.Polymorphic_entry (_, _) -> true in let typ = match proof_entry_type with - | None -> user_err Pp.(str "Admitted requires an explicit statement"); + | None -> CErrors.user_err Pp.(str "Admitted requires an explicit statement"); | Some typ -> typ in - let ctx = UState.univ_entry ~poly universes in + let ctx = UState.univ_entry ~poly uctx in let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in - finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms + finish_admitted ~name ~uctx ~info (sec_vars, (typ, ctx), None) -let save_lemma_proved_delayed ~proof ~info ~idopt = - (* Env and sigma are just used for error printing in save_remaining_recthms *) - let env = Global.env () in - let sigma = Evd.from_env env in - finalize_proof idopt env sigma proof info +let save_lemma_proved_delayed ~proof ~info ~idopt = finalize_proof idopt proof info diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index e790c39022..6a1f8c09f3 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -44,19 +44,6 @@ module Proof_ending : sig end -module Recthm : sig - type t = - { name : Id.t - (** Name of theorem *) - ; typ : EConstr.t - (** Type of theorem *) - ; args : Name.t list - (** Names to pre-introduce *) - ; impargs : Impargs.manual_implicits - (** Explicitily declared implicit arguments *) - } -end - module Info : sig type t @@ -95,7 +82,7 @@ val start_dependent_lemma type lemma_possible_guards = int list list -(** Pretty much internal, only used in ComFixpoint *) +(** Pretty much internal, used by the Lemma / Fixpoint vernaculars *) val start_lemma_with_initialization : ?hook:DeclareDef.Hook.t -> poly:bool @@ -103,8 +90,8 @@ val start_lemma_with_initialization -> kind:Decls.logical_kind -> udecl:UState.universe_decl -> Evd.evar_map - -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option - -> Recthm.t list + -> (bool * lemma_possible_guards * Constr.t option list option) option + -> DeclareDef.Recthm.t list -> int list option -> t diff --git a/vernac/library.ml b/vernac/library.ml index 877c10e69f..7c629b08e7 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/library.mli b/vernac/library.mli index ec485e6408..633d266821 100644 --- a/vernac/library.mli +++ b/vernac/library.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index 38aa42c349..d2df99e821 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/loadpath.mli b/vernac/loadpath.mli index 68212b9a47..cfd2becdc4 100644 --- a/vernac/loadpath.mli +++ b/vernac/loadpath.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/locality.ml b/vernac/locality.ml index c31f722a61..9e784c8bb3 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/locality.mli b/vernac/locality.mli index eda754324a..26149cb394 100644 --- a/vernac/locality.mli +++ b/vernac/locality.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 10946d78f0..475d5c31f7 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -252,7 +252,7 @@ let quote_notation_token x = let is_numeral symbs = match List.filter (function Break _ -> false | _ -> true) symbs with | ([Terminal "-"; Terminal x] | [Terminal x]) -> - NumTok.of_string x <> None + NumTok.Unsigned.parse_string x <> None | _ -> false diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index d76820b033..dd71817083 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 671dae7876..d276a1ac35 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/mltop.mli b/vernac/mltop.mli index 633a5c241d..b257fe7890 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 27eb821a6a..a29ba44907 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -17,18 +17,18 @@ open Printf - Apply term prefixed by quantification on "existentials". *) -open Term open Constr -open Vars open Names -open Evd open Pp open CErrors open Util module NamedDecl = Context.Named.Declaration +(* For the records fields, opens should go away one these types are private *) open DeclareObl +open DeclareObl.Obligation +open DeclareObl.ProgramDecl let succfix (depth, fixrels) = (succ depth, List.map succ fixrels) @@ -38,7 +38,7 @@ let check_evars env evm = (fun key evi -> if Evd.is_obligation_evar evm key then () else - let (loc,k) = evar_source key evm in + let (loc,k) = Evd.evar_source key evm in Pretype_errors.error_unsolvable_implicit ?loc env evm key None) (Evd.undefined_map evm) @@ -130,14 +130,14 @@ let etype_of_evar evm evs hyps concl = | LocalDef (id,c,_) -> let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in let c' = subst_vars acc 0 c' in - mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest, + Term.mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest, Int.Set.union s'' s', Id.Set.union trans'' trans' | LocalAssum (id,_) -> - mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') + Term.mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') | [] -> - let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in - subst_vars acc 0 t', s, trans + let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in + subst_vars acc 0 t', s, trans in aux [] 0 (List.rev hyps) let trunc_named_context n ctx = @@ -149,14 +149,14 @@ let rec chop_product n t = if Int.equal n 0 then Some t else match Constr.kind t with - | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (pop b) else None + | Prod (_, _, b) -> if Vars.noccurn 1 b then chop_product (pred n) (pop b) else None | _ -> None let evar_dependencies evm oev = let one_step deps = Evar.Set.fold (fun ev s -> let evi = Evd.find evm ev in - let deps' = evars_of_filtered_evar_info evm evi in + let deps' = Evd.evars_of_filtered_evar_info evm evi in if Evar.Set.mem oev deps' then invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev) else Evar.Set.union deps' s) @@ -189,8 +189,6 @@ let sort_dependencies evl = | [] -> List.rev list in aux evl Evar.Set.empty [] -open Environ - let eterm_obligations env name evm fs ?status t ty = (* 'Serialize' the evars *) let nc = Environ.named_context env in @@ -214,13 +212,13 @@ let eterm_obligations env name evm fs ?status t ty = (fun (id, (n, nstr), ev) l -> let hyps = Evd.evar_filtered_context ev in let hyps = trunc_named_context nc_len hyps in - let evtyp, deps, transp = etype_of_evar evm l hyps ev.evar_concl in + let evtyp, deps, transp = etype_of_evar evm l hyps ev.Evd.evar_concl in let evtyp, hyps, chop = match chop_product fs evtyp with | Some t -> t, trunc_named_context fs hyps, fs | None -> evtyp, hyps, 0 in - let loc, k = evar_source id evm in + let loc, k = Evd.evar_source id evm in let status = match k with | Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o | _ -> match status with @@ -281,75 +279,31 @@ let assumption_message = Declare.assumption_message let default_tactic = ref (Proofview.tclUNIT ()) -let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) +let evar_of_obligation o = Evd.make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) let subst_deps expand obls deps t = - let osubst = obl_substitution expand obls deps in + let osubst = DeclareObl.obl_substitution expand obls deps in (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) let subst_deps_obl obls obl = let t' = subst_deps true obls obl.obl_deps obl.obl_type in - { obl with obl_type = t' } + Obligation.set_type ~typ:t' obl open Evd -let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] - -let add_hint local prg cst = - Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst) - -let init_prog_info ?(opaque = false) ?hook n udecl b t ctx deps fixkind - notations obls impls ~scope ~poly ~kind reduce = - let obls', b = - match b with - | None -> - assert(Int.equal (Array.length obls) 0); - let n = Nameops.add_suffix n "_obligation" in - [| { obl_name = n; obl_body = None; - obl_location = Loc.tag Evar_kinds.InternalHole; obl_type = t; - obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty; - obl_tac = None } |], - mkVar n - | Some b -> - Array.mapi - (fun i (n, t, l, o, d, tac) -> - { obl_name = n ; obl_body = None; - obl_location = l; obl_type = t; obl_status = o; - obl_deps = d; obl_tac = tac }) - obls, b - in - let ctx = UState.make_flexible_nonalgebraic ctx in - { prg_name = n - ; prg_body = b - ; prg_type = reduce t - ; prg_ctx = ctx - ; prg_univdecl = udecl - ; prg_obligations = (obls', Array.length obls') - ; prg_deps = deps - ; prg_fixkind = fixkind - ; prg_notations = notations - ; prg_implicits = impls - ; prg_poly = poly - ; prg_scope = scope - ; prg_kind = kind - ; prg_reduce = reduce - ; prg_hook = hook - ; prg_opaque = opaque - } - let map_cardinal m = let i = ref 0 in ProgMap.iter (fun _ v -> - if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m; + if (CEphemeron.get v).prg_obligations.remaining > 0 then incr i) m; !i -exception Found of program_info CEphemeron.key +exception Found of ProgramDecl.t CEphemeron.key let map_first m = try ProgMap.iter (fun _ v -> - if snd (CEphemeron.get v).prg_obligations > 0 then - raise (Found v)) m; + if (CEphemeron.get v).prg_obligations.remaining > 0 then + raise (Found v)) m; assert(false) with Found x -> x @@ -416,16 +370,14 @@ let warn_solve_errored = CWarnings.create ~name:"solve_obligation_error" ~catego Pp.seq [str "Solve Obligations tactic returned error: "; err; fnl (); str "This will become an error in the future"]) -let solve_by_tac ?loc name evi t poly ctx = - (* spiwack: the status is dropped. *) +let solve_by_tac ?loc name evi t poly uctx = try - let (entry,_,ctx') = - Pfedit.build_constant_by_tactic - ~name ~poly ctx evi.evar_hyps evi.evar_concl t in + (* the status is dropped. *) let env = Global.env () in - let body, ctx' = Declare.inline_private_constants ~univs:ctx' env entry in - Inductiveops.control_only_guard env (Evd.from_ctx ctx') (EConstr.of_constr body); - Some (body, entry.Declare.proof_entry_type, ctx') + let body, types, _, uctx = + Pfedit.build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in + Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body); + Some (body, types, uctx) with | Refiner.FailError (_, s) as exn -> let _ = Exninfo.capture exn in @@ -438,43 +390,9 @@ let solve_by_tac ?loc name evi t poly ctx = warn_solve_errored ?loc err; None -let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } = - let obls, rem = prg.prg_obligations in - let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in - let transparent = evaluable_constant cst (Global.env ()) in - let () = match obl.obl_status with - (true, Evar_kinds.Expand) - | (true, Evar_kinds.Define true) -> - if not transparent then err_not_transp () - | _ -> () - in - let inst, ctx' = - if not prg.prg_poly (* Not polymorphic *) then - (* The universe context was declared globally, we continue - from the new global environment. *) - let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in - let ctx' = UState.merge_subst ctx (UState.subst ctx') in - Univ.Instance.empty, ctx' - else - (* We get the right order somehow, but surely it could be enforced in a clearer way. *) - let uctx = UState.context ctx' in - Univ.UContext.instance uctx, ctx' - in - let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in - let () = if transparent then add_hint true prg cst in - let obls = Array.copy obls in - let () = obls.(num) <- obl in - let prg = { prg with prg_ctx = ctx' } in - let () = ignore (update_obls prg obls (pred rem)) in - if pred rem > 0 then begin - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then - ignore (auto (Some prg.prg_name) deps None) - end - let rec solve_obligation prg num tac = let user_num = succ num in - let obls, rem = prg.prg_obligations in + let { obls; remaining=rem } = prg.prg_obligations in let obl = obls.(num) in let remaining = deps_remaining obls obl.obl_deps in let () = @@ -491,7 +409,7 @@ let rec solve_obligation prg num tac = let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n oblset tac = auto_solve_obligations n ~oblset tac in let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in - let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in + let hook = DeclareDef.Hook.make (DeclareObl.obligation_hook prg obl num auto) in let info = Lemmas.Info.make ~hook ~proof_ending ~scope ~kind () in let poly = prg.prg_poly in let lemma = Lemmas.start_lemma ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in @@ -502,7 +420,7 @@ let rec solve_obligation prg num tac = and obligation (user_num, name, typ) tac = let num = pred user_num in let prg = get_prog_err name in - let obls, rem = prg.prg_obligations in + let { obls; remaining } = prg.prg_obligations in if num >= 0 && num < Array.length obls then let obl = obls.(num) in match obl.obl_body with @@ -532,8 +450,9 @@ and solve_obligation_by_tac prg obls i tac = prg.prg_poly (Evd.evar_universe_context evd) with | None -> None | Some (t, ty, ctx) -> + let prg = ProgramDecl.set_uctx ~uctx:ctx prg in + (* Why is uctx not used above? *) let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in - let prg = {prg with prg_ctx = ctx} in let def, obl' = declare_obligation prg obl t ty uctx in obls.(i) <- obl'; if def && not prg.prg_poly then ( @@ -541,13 +460,13 @@ and solve_obligation_by_tac prg obls i tac = let evd = Evd.from_env (Global.env ()) in let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in let ctx' = Evd.evar_universe_context evd in - Some {prg with prg_ctx = ctx'}) + Some (ProgramDecl.set_uctx ~uctx:ctx' prg)) else Some prg else None and solve_prg_obligations prg ?oblset tac = - let obls, rem = prg.prg_obligations in - let rem = ref rem in + let { obls; remaining } = prg.prg_obligations in + let rem = ref remaining in let obls' = Array.copy obls in let set = ref Int.Set.empty in let p = match oblset with @@ -555,20 +474,20 @@ and solve_prg_obligations prg ?oblset tac = | Some s -> set := s; (fun i -> Int.Set.mem i !set) in - let prgref = ref prg in - let () = - Array.iteri (fun i x -> + let prg = + Array.fold_left_i (fun i prg x -> if p i then - match solve_obligation_by_tac !prgref obls' i tac with - | None -> () - | Some prg' -> - prgref := prg'; - let deps = dependencies obls i in - (set := Int.Set.union !set deps; - decr rem)) - obls' + match solve_obligation_by_tac prg obls' i tac with + | None -> prg + | Some prg -> + let deps = dependencies obls i in + set := Int.Set.union !set deps; + decr rem; + prg + else prg) + prg obls' in - update_obls !prgref obls' !rem + update_obls prg obls' !rem and solve_obligations n tac = let prg = get_prog_err n in @@ -579,10 +498,10 @@ and solve_all_obligations tac = and try_solve_obligation n prg tac = let prg = get_prog prg in - let obls, rem = prg.prg_obligations in + let {obls; remaining } = prg.prg_obligations in let obls' = Array.copy obls in match solve_obligation_by_tac prg obls' n tac with - | Some prg' -> ignore(update_obls prg' obls' (pred rem)) + | Some prg' -> ignore(update_obls prg' obls' (pred remaining)) | None -> () and try_solve_obligations n tac = @@ -595,9 +514,9 @@ and auto_solve_obligations n ?oblset tac : progress = open Pp let show_obligations_of_prg ?(msg=true) prg = let n = prg.prg_name in - let obls, rem = prg.prg_obligations in + let {obls; remaining} = prg.prg_obligations in let showed = ref 5 in - if msg then Feedback.msg_info (int rem ++ str " obligation(s) remaining: "); + if msg then Feedback.msg_info (int remaining ++ str " obligation(s) remaining: "); Array.iteri (fun i x -> match x.obl_body with | None -> @@ -630,12 +549,12 @@ let show_term n = Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ Printer.pr_constr_env env sigma prg.prg_body) -let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl) - ?(implicits=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic +let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl) + ?(impargs=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic ?(reduce=reduce) ?hook ?(opaque = false) obls = let info = Id.print name ++ str " has type-checked" in - let prg = init_prog_info ~opaque name univdecl term t ctx [] None [] obls implicits ~poly ~scope ~kind reduce ?hook in - let obls,_ = prg.prg_obligations in + let prg = ProgramDecl.make ~opaque name ~udecl term t ~uctx [] None [] obls ~impargs ~poly ~scope ~kind reduce ?hook in + let {obls;_} = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose Feedback.msg_info (info ++ str "."); let cst = DeclareObl.declare_definition prg in @@ -649,14 +568,14 @@ let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl) | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some name)) (); res | _ -> res) -let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic +let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce) ?hook ?(opaque = false) notations fixkind = let deps = List.map (fun (n, b, t, imps, obls) -> n) l in List.iter - (fun (n, b, t, imps, obls) -> - let prg = init_prog_info ~opaque n univdecl (Some b) t ctx deps (Some fixkind) - notations obls imps ~poly ~scope ~kind reduce ?hook + (fun (n, b, t, impargs, obls) -> + let prg = ProgramDecl.make ~opaque n ~udecl (Some b) t ~uctx deps (Some fixkind) + notations obls ~impargs ~poly ~scope ~kind reduce ?hook in progmap_add n (CEphemeron.create prg)) l; let _defined = List.fold_left (fun finished x -> @@ -672,7 +591,7 @@ let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic in () let admit_prog prg = - let obls, rem = prg.prg_obligations in + let {obls; remaining} = prg.prg_obligations in let obls = Array.copy obls in Array.iteri (fun i x -> @@ -684,10 +603,10 @@ let admit_prog prg = (Declare.ParameterEntry (None,(x.obl_type,ctx),None)) ~kind:Decls.(IsAssumption Conjectural) in assumption_message x.obl_name; - obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) } + obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x | Some _ -> ()) obls; - ignore(update_obls prg obls 0) + ignore(DeclareObl.update_obls prg obls 0) let rec admit_all_obligations () = let prg = try Some (get_any_prog ()) with NoObligations _ -> None in @@ -709,7 +628,7 @@ let next_obligation n tac = | None -> get_any_prog_err () | Some _ -> get_prog_err n in - let obls, rem = prg.prg_obligations in + let {obls; remaining} = prg.prg_obligations in let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in let i = match Array.findi is_open obls with | Some i -> i diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 2a0d0aba97..101958072a 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -51,9 +51,9 @@ val default_tactic : unit Proofview.tactic ref val add_definition : name:Names.Id.t -> ?term:constr -> types - -> UState.t - -> ?univdecl:UState.universe_decl (* Universe binders and constraints *) - -> ?implicits:Impargs.manual_implicits + -> uctx:UState.t + -> ?udecl:UState.universe_decl (* Universe binders and constraints *) + -> ?impargs:Impargs.manual_implicits -> poly:bool -> ?scope:DeclareDef.locality -> ?kind:Decls.definition_object_kind @@ -65,9 +65,10 @@ val add_definition -> DeclareObl.progress val add_mutual_definitions + (* XXX: unify with MutualEntry *) : (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list - -> UState.t - -> ?univdecl:UState.universe_decl + -> uctx:UState.t + -> ?udecl:UState.universe_decl (** Universe binders and constraints *) -> ?tactic:unit Proofview.tactic -> poly:bool diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 84ae04e4cc..054b60853f 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -142,7 +142,7 @@ open Pputils | SearchOutside [] -> mt() | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l - let pr_search_about (b,c) = + let pr_search (b,c) = (if b then str "-" else mt()) ++ match c with | SearchSubPattern p -> @@ -158,10 +158,8 @@ open Pputils | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b - | SearchAbout sl -> - keyword "SearchAbout" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b | Search sl -> - keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b + keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search sl ++ pr_in_out_modules b let pr_option_ref_value = function | QualidRefValue id -> pr_qualid id @@ -804,7 +802,7 @@ let string_of_definition_object_kind = let open Decls in function let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in return (hov 2 (pr_assumption_token (n > 1) discharge kind ++ pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions)) - | VernacInductive (cum, p,f,l) -> + | VernacInductive (f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ @@ -830,24 +828,14 @@ let string_of_definition_object_kind = let open Decls in function str" :=") ++ pr_constructor_list lc ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn in - let key = - let kind = - match f with Record -> "Record" | Structure -> "Structure" - | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" - | Class _ -> "Class" | Variant -> "Variant" - in - if p then - let cm = - match cum with - | Some VernacCumulative -> "Cumulative" - | Some VernacNonCumulative -> "NonCumulative" - | None -> "" - in - cm ^ " " ^ kind - else kind + let kind = + match f with + | Record -> "Record" | Structure -> "Structure" + | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" + | Class _ -> "Class" | Variant -> "Variant" in return ( - hov 1 (pr_oneind key (List.hd l)) ++ + hov 1 (pr_oneind kind (List.hd l)) ++ (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) ) diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli index 9ade5afb87..9339803948 100644 --- a/vernac/ppvernac.mli +++ b/vernac/ppvernac.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index cdd93db884..a7170c8e18 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -83,6 +83,8 @@ let print_ref reduce ref udecl = let ctx,ccl = Reductionops.splay_prod_assum env sigma typ in EConstr.it_mkProd_or_LetIn ccl ctx else typ in + let impargs = select_stronger_impargs (implicits_of_global ref) in + let impargs = List.map binding_kind_of_status impargs in let variance = let open GlobRef in match ref with | VarRef _ | ConstRef _ -> None | IndRef (ind,_) | ConstructRef ((ind,_),_) -> @@ -95,7 +97,7 @@ let print_ref reduce ref udecl = else mt () in let priv = None in (* We deliberately don't print private univs in About. *) - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma ~impargs typ ++ Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv) (********************************) diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli index ac41f30c5d..19a4958350 100644 --- a/vernac/prettyp.mli +++ b/vernac/prettyp.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index b329463cb0..2130a398e9 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli index a0567eef47..dfc233e8fa 100644 --- a/vernac/proof_using.mli +++ b/vernac/proof_using.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 2425f3d6c1..08625b41a6 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index 3bd252ecef..4de12f5e3b 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml index e6d428968c..eb0e1fb795 100644 --- a/vernac/recLemmas.ml +++ b/vernac/recLemmas.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/recLemmas.mli b/vernac/recLemmas.mli index dfb5e4a644..1a697c1e88 100644 --- a/vernac/recLemmas.mli +++ b/vernac/recLemmas.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/record.ml b/vernac/record.ml index 065641989d..d974ead942 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -613,7 +613,7 @@ let add_constant_class env sigma cst = } in Classes.add_class env sigma tc; - set_typeclass_transparency (EvalConstRef cst) false false + Classes.set_typeclass_transparency (EvalConstRef cst) false false let add_inductive_class env sigma ind = let mind, oneind = Inductive.lookup_mind_specif env ind in diff --git a/vernac/record.mli b/vernac/record.mli index 571fd9536e..e890f80150 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/search.ml b/vernac/search.ml index b8825c3b29..68a30b4231 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -23,8 +23,8 @@ module NamedDecl = Context.Named.Declaration type filter_function = GlobRef.t -> env -> constr -> bool type display_function = GlobRef.t -> env -> constr -> unit -(* This option restricts the output of [SearchPattern ...], -[SearchAbout ...], etc. to the names of the symbols matching the +(* This option restricts the output of [SearchPattern ...], etc. +to the names of the symbols matching the query, separated by a newline. This type of output is useful for editors (like emacs), to generate a list of completion candidates without having to parse through the types of all symbols. *) @@ -226,7 +226,7 @@ let module_filter (mods, outside) ref env typ = let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref) -let search_about_filter query gr env typ = match query with +let search_filter query gr env typ = match query with | GlobSearchSubPattern pat -> Constr_matching.is_matching_appsubterm ~closed:false env (Evd.from_env env) pat (EConstr.of_constr typ) | GlobSearchString s -> @@ -283,14 +283,14 @@ let search_by_head ?pstate gopt pat mods pr_search = in generic_search ?pstate gopt iter -(** SearchAbout *) +(** Search *) -let search_about ?pstate gopt items mods pr_search = +let search ?pstate gopt items mods pr_search = let filter ref env typ = let eqb b1 b2 = if b1 then b2 else not b2 in module_filter mods ref env typ && List.for_all - (fun (b,i) -> eqb b (search_about_filter i ref env typ)) items && + (fun (b,i) -> eqb b (search_filter i ref env typ)) items && blacklist_filter ref env typ in let iter ref env typ = diff --git a/vernac/search.mli b/vernac/search.mli index 029e8cf7b9..6dbbff3a8c 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -30,8 +30,7 @@ val blacklist_filter : filter_function val module_filter : DirPath.t list * bool -> filter_function (** Check whether a reference pertains or not to a set of modules *) -val search_about_filter : glob_search_about_item -> filter_function -(** Check whether a reference matches a SearchAbout query. *) +val search_filter : glob_search_about_item -> filter_function (** {6 Specialized search functions} @@ -45,7 +44,7 @@ val search_rewrite : ?pstate:Proof_global.t -> int option -> constr_pattern -> D -> display_function -> unit val search_pattern : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool -> display_function -> unit -val search_about : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list +val search : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list -> DirPath.t list * bool -> display_function -> unit type search_constraint = diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 509c164af8..2d8734ff7f 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index dc4642dc65..c54e75e8cc 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 953faf6fdb..963b5f2084 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -15,17 +15,10 @@ open CErrors open CAst open Util open Names -open Tacmach -open Constrintern -open Prettyp open Printer open Goptions open Libnames -open Globnames open Vernacexpr -open Constrexpr -open Redexpr -open Lemmas open Locality open Attributes @@ -128,7 +121,7 @@ let show_intro ~proof all = let Proof.{goals;sigma} = Proof.data proof in if not (List.is_empty goals) then begin let gl = {Evd.it=List.hd goals ; sigma = sigma; } in - let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in + let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (Tacmach.pf_concl gl)) in if all then let lid = Tactics.find_intro_names l gl in hov 0 (prlist_with_sep spc Id.print lid) @@ -480,11 +473,14 @@ let program_inference_hook env sigma ev = let concl = evi.Evd.evar_concl in if not (Evarutil.is_ground_env sigma env && Evarutil.is_ground_term sigma concl) - then raise Exit; - let c, _, ctx = - Pfedit.build_by_tactic ~poly:false env (Evd.evar_universe_context sigma) concl tac - in Evd.set_universe_context sigma ctx, EConstr.of_constr c - with Logic_monad.TacticFailure e when Logic.catchable_exception e -> + then None + else + let c, _, _, ctx = + Pfedit.build_by_tactic ~poly:false env ~uctx:(Evd.evar_universe_context sigma) ~typ:concl tac + in + Some (Evd.set_universe_context sigma ctx, EConstr.of_constr c) + with + | Logic_monad.TacticFailure e when noncritical e -> user_err Pp.(str "The statement obligations could not be resolved \ automatically, write a statement definition first.") @@ -493,24 +489,19 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = let decl = fst (List.hd thms) in let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) -> - let evd, (impls, ((env, ctx), imps)) = interp_context_evars ~program_mode env0 evd bl in - let evd, (t', imps') = interp_type_evars_impls ~program_mode ~impls env evd t in + let evd, (impls, ((env, ctx), imps)) = Constrintern.interp_context_evars ~program_mode env0 evd bl in + let evd, (t', imps') = Constrintern.interp_type_evars_impls ~program_mode ~impls env evd t in let flags = Pretyping.{ all_and_fail_flags with program_mode } in let inference_hook = if program_mode then Some program_inference_hook else None in let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in let ids = List.map Context.Rel.Declaration.get_name ctx in check_name_freshness scope id; - (* XXX: The nf_evar is critical !! *) - evd, (id.CAst.v, - (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), - (ids, imps @ imps')))) + evd, (id.CAst.v, (EConstr.it_mkProd_or_LetIn t' ctx, (ids, imps @ imps')))) evd thms in let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in let evd = Evd.minimize_universes evd in - (* XXX: This nf_evar is critical too!! We are normalizing twice if - you look at the previous lines... *) let thms = List.map (fun (name, (typ, (args, impargs))) -> - { Recthm.name; typ = Evarutil.nf_evar evd typ; args; impargs} ) thms in + { DeclareDef.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in let () = let open UState in if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then @@ -521,7 +512,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = else (* We fix the variables to ensure they won't be lowered to Set *) Evd.fix_undefined_variables evd in - start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl + Lemmas.start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function | Coercion -> @@ -587,15 +578,15 @@ let vernac_start_proof ~atts kind l = let vernac_end_proof ~lemma = let open Vernacexpr in function | Admitted -> - save_lemma_admitted ~lemma + Lemmas.save_lemma_admitted ~lemma | Proved (opaque,idopt) -> - save_lemma_proved ~lemma ~opaque ~idopt + Lemmas.save_lemma_proved ~lemma ~opaque ~idopt let vernac_exact_proof ~lemma c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the beginning of a proof. *) let lemma, status = Lemmas.by (Tactics.exact_proof c) lemma in - let () = save_lemma_proved ~lemma ~opaque:Proof_global.Opaque ~idopt:None in + let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Opaque ~idopt:None in if not status then Feedback.feedback Feedback.AddedAxiom let vernac_assumption ~atts discharge kind l nl = @@ -611,17 +602,39 @@ let vernac_assumption ~atts discharge kind l nl = let is_polymorphic_inductive_cumulativity = declare_bool_option_and_ref ~depr:false ~value:false - ~key:["Polymorphic"; "Inductive"; "Cumulativity"] - -let should_treat_as_cumulative cum poly = - match cum with - | Some VernacCumulative -> - if poly then true - else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.") - | Some VernacNonCumulative -> - if poly then false - else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") - | None -> poly && is_polymorphic_inductive_cumulativity () + ~key:["Polymorphic";"Inductive";"Cumulativity"] + +let polymorphic_cumulative = + let error_poly_context () = + user_err + Pp.(str "The cumulative and noncumulative attributes can only be used in a polymorphic context."); + in + let open Attributes in + let open Notations in + qualify_attribute "universes" + (bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic" + ++ bool_attribute ~name:"Cumulativity" ~on:"cumulative" ~off:"noncumulative") + >>= function + | Some poly, Some cum -> + (* Case of Polymorphic|Monomorphic Cumulative|NonCumulative Inductive + and #[ universes(polymorphic|monomorphic,cumulative|noncumulative) ] Inductive *) + if poly then return (true, cum) + else error_poly_context () + | Some poly, None -> + (* Case of Polymorphic|Monomorphic Inductive + and #[ universes(polymorphic|monomorphic) ] Inductive *) + if poly then return (true, is_polymorphic_inductive_cumulativity ()) + else return (false, false) + | None, Some cum -> + (* Case of Cumulative|NonCumulative Inductive *) + if is_universe_polymorphism () then return (true, cum) + else error_poly_context () + | None, None -> + (* Case of Inductive *) + if is_universe_polymorphism () then + return (true, is_polymorphic_inductive_cumulativity ()) + else + return (false, false) let get_uniform_inductive_parameters = Goptions.declare_bool_option_and_ref @@ -634,8 +647,7 @@ let should_treat_as_uniform () = then ComInductive.UniformParameters else ComInductive.NonUniformParameters -let vernac_record ~template udecl cum k poly finite records = - let cumulative = should_treat_as_cumulative cum poly in +let vernac_record ~template udecl ~cumulative k ~poly finite records = let map ((coe, id), binders, sort, nameopt, cfs) = let const = match nameopt with | None -> Nameops.add_prefix "Build_" id.v @@ -675,12 +687,21 @@ let finite_of_kind = let open Declarations in function | CoInductive -> CoFinite | Variant | Record | Structure | Class _ -> BiFinite -(** When [poly] is true the type is declared polymorphic. When [lo] is true, - then the type is declared private (as per the [Private] keyword). [finite] - indicates whether the type is inductive, co-inductive or - neither. *) -let vernac_inductive ~atts cum lo kind indl = - let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in +let private_ind = + let open Attributes in + let open Notations in + attribute_of_list + [ "matching" + , single_key_parser ~name:"Private (matching) inductive type" ~key:"matching" () + ] + |> qualify_attribute "private" + >>= function + | Some () -> return true + | None -> return false + +let vernac_inductive ~atts kind indl = + let (template, (poly, cumulative)), private_ind = Attributes.( + parse Notations.(template ++ polymorphic_cumulative ++ private_ind) atts) in let open Pp in let udecl, indl = extract_inductive_udecl indl in if Dumpglob.dump () then @@ -717,7 +738,7 @@ let vernac_inductive ~atts cum lo kind indl = let coe' = if coe then Some true else None in let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce), { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in - vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]] + vernac_record ~template udecl ~cumulative (Class true) ~poly finite [id, bl, c, None, [f]] else if List.for_all is_record indl then (* Mutual record case *) let () = match kind with @@ -742,7 +763,7 @@ let vernac_inductive ~atts cum lo kind indl = in let kind = match kind with Class _ -> Class false | _ -> kind in let recordl = List.map unpack indl in - vernac_record ~template udecl cum kind poly finite recordl + vernac_record ~template udecl ~cumulative kind ~poly finite recordl else if List.for_all is_constructor indl then (* Mutual inductive case *) let () = match kind with @@ -765,9 +786,8 @@ let vernac_inductive ~atts cum lo kind indl = | RecordDecl _ -> assert false (* ruled out above *) in let indl = List.map unpack indl in - let cumulative = should_treat_as_cumulative cum poly in let uniform = should_treat_as_uniform () in - ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind:lo ~uniform finite + ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") @@ -825,7 +845,7 @@ let vernac_scheme l = let vernac_combined_scheme lid l = if Dumpglob.dump () then (Dumpglob.dump_definition lid false "def"; - List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (qualid_of_ident ?loc id))) l); + List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ Constrexpr.AN (qualid_of_ident ?loc id))) l); Indschemes.do_combined_scheme lid l let vernac_universe ~poly l = @@ -963,7 +983,7 @@ let vernac_begin_section ~poly ({v=id} as lid) = to its current value ie noop. *) set_bool_option_value_gen ~locality:OptLocal ["Universe"; "Polymorphism"] poly -let vernac_end_section {CAst.loc} = +let vernac_end_section {CAst.loc; v} = Dumpglob.dump_reference ?loc (DirPath.to_string (Lib.current_dirpath true)) "<>" "sec"; Lib.close_section () @@ -973,6 +993,7 @@ let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set (* Dispatcher of the "End" command *) let vernac_end_segment ({v=id} as lid) = + DeclareObl.check_can_close lid.v; match Lib.find_opening_node id with | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid @@ -1185,9 +1206,19 @@ let vernac_hints ~atts dbnames h = (warn_implicit_core_hint_db (); ["core"]) else dbnames in - let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in - let local = enforce_module_locality local in - Hints.add_hints ~local dbnames (Hints.interp_hints ~poly h) + let locality, poly = Attributes.(parse Notations.(option_locality ++ polymorphic) atts) in + let () = match locality with + | OptGlobal -> + if Global.sections_are_opened () then + CErrors.user_err Pp.(str + "This command does not support the global attribute in sections."); + | OptExport -> + if Global.sections_are_opened () then + CErrors.user_err Pp.(str + "This command does not support the export attribute in sections."); + | OptDefault | OptLocal -> () + in + Hints.add_hints ~locality dbnames (Hints.interp_hints ~poly h) let vernac_syntactic_definition ~atts lid x only_parsing = let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in @@ -1461,40 +1492,29 @@ let vernac_set_opacity ~local (v,l) = let l = List.map glob_ref l in Redexpr.set_strategy local [v,l] -let get_option_locality export local = - if export then - if Option.is_empty local then OptExport - else user_err Pp.(str "Locality modifiers forbidden with Export") - else match local with - | Some true -> OptLocal - | Some false -> OptGlobal - | None -> OptDefault - -let vernac_set_option0 ~local export key opt = - let locality = get_option_locality export local in +let vernac_set_option0 ~locality key opt = match opt with | OptionUnset -> unset_option_value_gen ~locality key | OptionSetString s -> set_string_option_value_gen ~locality key s | OptionSetInt n -> set_int_option_value_gen ~locality key (Some n) | OptionSetTrue -> set_bool_option_value_gen ~locality key true -let vernac_set_append_option ~local export key s = - let locality = get_option_locality export local in +let vernac_set_append_option ~locality key s = set_string_option_append_value_gen ~locality key s -let vernac_set_option ~local export table v = match v with +let vernac_set_option ~locality table v = match v with | OptionSetString s -> (* We make a special case for warnings because appending is their natural semantics *) if CString.List.equal table ["Warnings"] then - vernac_set_append_option ~local export table s + vernac_set_append_option ~locality table s else let (last, prefix) = List.sep_last table in if String.equal last "Append" && not (List.is_empty prefix) then - vernac_set_append_option ~local export prefix s + vernac_set_append_option ~locality prefix s else - vernac_set_option0 ~local export table v -| _ -> vernac_set_option0 ~local export table v + vernac_set_option0 ~locality table v +| _ -> vernac_set_option0 ~locality table v let vernac_add_option key lv = let f = function @@ -1543,7 +1563,7 @@ let query_command_selector ?loc = function let vernac_check_may_eval ~pstate ~atts redexp glopt rc = let glopt = query_command_selector glopt in let sigma, env = get_current_context_of_args ~pstate glopt in - let sigma, c = interp_open_constr ~expected_type:Pretyping.UnknownIfTermOrType env sigma rc in + let sigma, c = Constrintern.interp_open_constr ~expected_type:Pretyping.UnknownIfTermOrType env sigma rc in let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in Evarconv.check_problems_are_solved env sigma; let sigma = Evd.minimize_universes sigma in @@ -1562,16 +1582,16 @@ let vernac_check_may_eval ~pstate ~atts redexp glopt rc = let evars_of_term c = Evarutil.undefined_evars_of_term sigma c in let l = Evar.Set.union (evars_of_term j.Environ.uj_val) (evars_of_term j.Environ.uj_type) in let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma j.Environ.uj_type } in - print_judgment env sigma j ++ + Prettyp.print_judgment env sigma j ++ pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma l | Some r -> let (sigma,r_interp) = Hook.get f_interp_redexp env sigma r in let redfun env evm c = - let (redfun, _) = reduction_of_red_expr env r_interp in + let (redfun, _) = Redexpr.reduction_of_red_expr env r_interp in let (_, c) = redfun env evm c in c in - print_eval redfun env sigma rc j + Prettyp.print_eval redfun env sigma rc j in pp ++ Printer.pr_universe_ctx_set sigma uctx @@ -1579,20 +1599,20 @@ let vernac_declare_reduction ~local s r = let local = Option.default false local in let env = Global.env () in let sigma = Evd.from_env env in - declare_red_expr local s (snd (Hook.get f_interp_redexp env sigma r)) + Redexpr.declare_red_expr local s (snd (Hook.get f_interp_redexp env sigma r)) (* The same but avoiding the current goal context if any *) let vernac_global_check c = let env = Global.env() in let sigma = Evd.from_env env in - let c,uctx = interp_constr env sigma c in + let c,uctx = Constrintern.interp_constr env sigma c in let senv = Global.safe_env() in let uctx = UState.context_set uctx in let senv = Safe_typing.push_context_set ~strict:false uctx senv in let c = EConstr.to_constr sigma c in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in - print_safe_judgment env sigma j ++ + Prettyp.print_safe_judgment env sigma j ++ pr_universe_ctx_set sigma uctx @@ -1602,12 +1622,11 @@ let get_nth_goal ~pstate n = let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in gl -exception NoHyp - (* Printing "About" information of a hypothesis of the current goal. We only print the type and a small statement to this comes from the goal. Precondition: there must be at least one current goal. *) let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = + let exception NoHyp in let open Context.Named.Declaration in try (* Fallback early to globals *) @@ -1618,6 +1637,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = (* FIXME error on non None udecl if we find the hyp. *) let glnumopt = query_command_selector ?loc glopt in let gl,id = + let open Constrexpr in match glnumopt, ref_or_by_not.v with | None,AN qid when qualid_is_ident qid -> (* goal number not given, catch any failure *) (try get_nth_goal ~pstate 1, qualid_basename qid with _ -> raise NoHyp) @@ -1627,7 +1647,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs" (str "No such goal: " ++ int n ++ str ".")) | _ , _ -> raise NoHyp in - let hyps = pf_hyps gl in + let hyps = Tacmach.pf_hyps gl in let decl = Context.Named.lookup id hyps in let natureofid = match decl with | LocalAssum _ -> "Hypothesis" @@ -1638,16 +1658,16 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = with (* fallback to globals *) | NoHyp | Not_found -> let sigma, env = get_current_or_global_context ~pstate in - print_about env sigma ref_or_by_not udecl + Prettyp.print_about env sigma ref_or_by_not udecl let vernac_print ~pstate ~atts = let sigma, env = get_current_or_global_context ~pstate in function | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ())) | PrintTables -> print_tables () - | PrintFullContext-> print_full_context_typ env sigma - | PrintSectionContext qid -> print_sec_context_typ env sigma qid - | PrintInspect n -> inspect env sigma n + | PrintFullContext-> Prettyp.print_full_context_typ env sigma + | PrintSectionContext qid -> Prettyp.print_sec_context_typ env sigma qid + | PrintInspect n -> Prettyp.inspect env sigma n | PrintGrammar ent -> Metasyntax.pr_grammar ent | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir @@ -1660,7 +1680,7 @@ let vernac_print ~pstate ~atts = | PrintDebugGC -> Mltop.print_gc () | PrintName (qid,udecl) -> dump_global qid; - print_name env sigma qid udecl + Prettyp.print_name env sigma qid udecl | PrintGraph -> Prettyp.print_graph () | PrintClasses -> Prettyp.print_classes() | PrintTypeClasses -> Prettyp.print_typeclasses() @@ -1692,11 +1712,11 @@ let vernac_print ~pstate ~atts = print_about_hyp_globs ~pstate ref_or_by_not udecl glnumopt | PrintImplicit qid -> dump_global qid; - print_impargs qid + Prettyp.print_impargs qid | PrintAssumptions (o,t,r) -> (* Prints all the axioms and section variables used by a term *) let gr = smart_global r in - let cstr = printable_constr_of_global gr in + let cstr = Globnames.printable_constr_of_global gr in let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in let nassums = Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in @@ -1719,7 +1739,7 @@ open Search let interp_search_about_item env sigma = function | SearchSubPattern pat -> - let _,pat = intern_constr_pattern env sigma pat in + let _,pat = Constrintern.intern_constr_pattern env sigma pat in GlobSearchSubPattern pat | SearchString (s,None) when Id.is_valid s -> GlobSearchString s @@ -1753,10 +1773,6 @@ let () = optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } -let warn_deprecated_search_about = - CWarnings.create ~name:"deprecated-search-about" ~category:"deprecated" - (fun () -> strbrk "The SearchAbout command is deprecated. Please use Search instead.") - let vernac_search ~pstate ~atts s gopt r = let gopt = query_command_selector gopt in let r = interp_search_restriction r in @@ -1768,43 +1784,43 @@ let vernac_search ~pstate ~atts s gopt r = (* if goal selector is given and wrong, then let exceptions be raised. *) | Some g -> snd (get_goal_or_global_context ~pstate g) , Some g in - let get_pattern c = snd (intern_constr_pattern env Evd.(from_env env) c) in + let get_pattern c = snd (Constrintern.intern_constr_pattern env Evd.(from_env env) c) in let pr_search ref env c = let pr = pr_global ref in let pp = if !search_output_name_only then pr else begin - let pc = pr_lconstr_env env Evd.(from_env env) c in + let open Impargs in + let impargs = select_stronger_impargs (implicits_of_global ref) in + let impargs = List.map binding_kind_of_status impargs in + let pc = pr_ltype_env env Evd.(from_env env) ~impargs c in hov 2 (pr ++ str":" ++ spc () ++ pc) end in Feedback.msg_notice pp in - match s with + (match s with | SearchPattern c -> (Search.search_pattern ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchRewrite c -> (Search.search_rewrite ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchHead c -> (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search - | SearchAbout sl -> - warn_deprecated_search_about (); - (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> - Search.prioritize_search) pr_search | Search sl -> - (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> - Search.prioritize_search) pr_search + (Search.search ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> + Search.prioritize_search) pr_search); + Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)") -let vernac_locate ~pstate = function - | LocateAny {v=AN qid} -> print_located_qualid qid - | LocateTerm {v=AN qid} -> print_located_term qid +let vernac_locate ~pstate = let open Constrexpr in function + | LocateAny {v=AN qid} -> Prettyp.print_located_qualid qid + | LocateTerm {v=AN qid} -> Prettyp.print_located_term qid | LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *) | LocateTerm {v=ByNotation (ntn, sc)} -> let _, env = get_current_or_global_context ~pstate in Notation.locate_notation (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc | LocateLibrary qid -> print_located_library qid - | LocateModule qid -> print_located_module qid - | LocateOther (s, qid) -> print_located_other s qid + | LocateModule qid -> Prettyp.print_located_module qid + | LocateOther (s, qid) -> Prettyp.print_located_other s qid | LocateFile f -> locate_file f let vernac_register qid r = @@ -2000,8 +2016,8 @@ let translate_vernac ~atts v = let open Vernacextend in match v with vernac_declare_module_type lid bl mtys mtyo) | VernacAssumption ((discharge,kind),nl,l) -> VtDefault(fun () -> with_def_attributes ~atts vernac_assumption discharge kind l nl) - | VernacInductive (cum, priv, finite, l) -> - VtDefault(fun () -> vernac_inductive ~atts cum priv finite l) + | VernacInductive (finite, l) -> + VtDefault(fun () -> vernac_inductive ~atts finite l) | VernacFixpoint (discharge, l) -> let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in if opens then @@ -2156,9 +2172,10 @@ let translate_vernac ~atts v = let open Vernacextend in match v with VtDefault(fun () -> with_locality ~atts vernac_set_opacity qidl) | VernacSetStrategy l -> VtDefault(fun () -> with_locality ~atts vernac_set_strategy l) - | VernacSetOption (export, key,v) -> + | VernacSetOption (export,key,v) -> + let atts = if export then ("export", VernacFlagEmpty) :: atts else atts in VtDefault(fun () -> - vernac_set_option ~local:(only_locality atts) export key v) + vernac_set_option ~locality:(parse option_locality atts) key v) | VernacRemoveOption (key,v) -> VtDefault(fun () -> unsupported_attributes atts; diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 6368ebeed8..f5cf9702cd 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 7169ea834a..d6e7a3947a 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -69,7 +69,6 @@ type searchable = | SearchPattern of constr_pattern_expr | SearchRewrite of constr_pattern_expr | SearchHead of constr_pattern_expr - | SearchAbout of (bool * search_about_item) list | Search of (bool * search_about_item) list type locatable = @@ -250,10 +249,6 @@ type register_kind = type module_ast_inl = module_ast * Declaremods.inline type module_binder = bool option * lident list * module_ast_inl -(** [Some b] if locally enabled/disabled according to [b], [None] if - we should use the global flag. *) -type vernac_cumulative = VernacCumulative | VernacNonCumulative - (** {6 The type of vernacular expressions} *) type vernac_one_argument_status = { @@ -312,7 +307,7 @@ type nonrec vernac_expr = | VernacExactProof of constr_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_kind * (inductive_expr * decl_notation list) list + | VernacInductive of inductive_kind * (inductive_expr * decl_notation list) list | VernacFixpoint of discharge * fixpoint_expr list | VernacCoFixpoint of discharge * cofixpoint_expr list | VernacScheme of (lident option * scheme) list @@ -403,7 +398,7 @@ type nonrec vernac_expr = | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list) | VernacSetStrategy of (Conv_oracle.level * qualid or_by_notation list) list - | VernacSetOption of export_flag * Goptions.option_name * option_setting + | VernacSetOption of bool (* Export modifier? *) * Goptions.option_name * option_setting | VernacAddOption of Goptions.option_name * option_ref_value list | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 5d38ea32be..0e8202da9f 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 3df74e5f2c..90c00415d4 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 8083098022..15a19c06c2 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index 16849686da..9f5bfb46ee 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 903a28e953..a632d860a7 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli index 320878e401..352c81b8b4 100644 --- a/vernac/vernacprop.mli +++ b/vernac/vernacprop.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 280343f315..6846826bfa 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index b4322eb09a..7607f8373a 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |