diff options
81 files changed, 519 insertions, 468 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index f422030b53..50d4d21637 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -238,7 +238,7 @@ ######################################################################## # plugin_tutorial ######################################################################## -: "${plugin_tutorial_CI_REF:=14b2976cdf67db788b79d9421ce1e89bd15c7313}" +: "${plugin_tutorial_CI_REF:=master}" : "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}" : "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}" diff --git a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh new file mode 100644 index 0000000000..bd3e1bf7ff --- /dev/null +++ b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8741" ] || [ "$CI_BRANCH" = "typeclasses-functional-evar_map" ]; then + plugin_tutorial_CI_REF=pr8671-fix + plugin_tutorial_CI_GITURL=https://github.com/mattam82/plugin_tutorials + +fi diff --git a/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh b/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh new file mode 100644 index 0000000000..98530c825a --- /dev/null +++ b/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "8684" ] || [ "$CI_BRANCH" = "kernel-entries-cleanup" ]; then + + Elpi_CI_REF=kernel-entries-cleanup + Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi + + Equations_CI_REF=kernel-entries-cleanup + Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations + +fi diff --git a/engine/evarutil.ml b/engine/evarutil.ml index f9d9ce3569..4e1636e321 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -405,12 +405,13 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ = let default_source = Loc.tag @@ Evar_kinds.InternalHole -let new_pure_evar_full evd evi = - let (evd, evk) = Evd.new_evar evd evi in +let new_pure_evar_full evd ?typeclass_candidate evi = + let (evd, evk) = Evd.new_evar evd ?typeclass_candidate evi in let evd = Evd.declare_future_goal evk evd in (evd, evk) -let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ = +let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?typeclass_candidate + ?(principal=false) sign evd typ = let default_naming = IntroAnonymous in let naming = Option.default default_naming naming in let name = match naming with @@ -427,34 +428,34 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ? evar_body = Evar_empty; evar_filter = filter; evar_source = src; - evar_candidates = candidates; - evar_extra = store; } + evar_candidates = candidates } in - let (evd, newevk) = Evd.new_evar evd ?name evi in + let typeclass_candidate = if principal then Some false else typeclass_candidate in + let (evd, newevk) = Evd.new_evar evd ?name ?typeclass_candidate evi in let evd = if principal then Evd.declare_principal_goal newevk evd else Evd.declare_future_goal newevk evd in (evd, newevk) -let new_evar_instance ?src ?filter ?candidates ?store ?naming ?principal sign evd typ instance = +let new_evar_instance ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ instance = let open EConstr in assert (not !Flags.debug || List.distinct (ids_of_named_context (named_context_of_val sign))); - let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in + let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal typ in evd, mkEvar (newevk,Array.of_list instance) -let new_evar_from_context ?src ?filter ?candidates ?store ?naming ?principal sign evd typ = +let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ = let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in let instance = match filter with | None -> instance | Some filter -> Filter.filter_list filter instance in - new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance + new_evar_instance sign evd typ ?src ?filter ?candidates ?naming ?principal instance (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env evd typ = +let new_evar ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal ?hypnaming env evd typ = let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in let map c = csubst_subst subst c in let candidates = Option.map (fun l -> List.map map l) candidates in @@ -462,11 +463,11 @@ let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env e match filter with | None -> instance | Some filter -> Filter.filter_list filter instance in - new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance + new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal instance let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid = let (evd', s) = new_sort_variable rigid evd in - let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in + let (evd', e) = new_evar env evd' ?src ?filter ?naming ~typeclass_candidate:false ?principal ?hypnaming (EConstr.mkSort s) in evd', (e, s) let new_Type ?(rigid=Evd.univ_flexible) evd = @@ -714,7 +715,7 @@ let rec advance sigma evk = match evi.evar_body with | Evar_empty -> Some evk | Evar_defined v -> - match is_restricted_evar evi with + match is_restricted_evar sigma evk with | Some evk -> advance sigma evk | None -> None diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 11e07175e3..0c8d8c9b8a 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -27,8 +27,9 @@ val mk_new_meta : unit -> constr val new_evar_from_context : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> + ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> + ?typeclass_candidate:bool -> ?principal:bool -> named_context_val -> evar_map -> types -> evar_map * EConstr.t @@ -40,19 +41,21 @@ type naming_mode = val new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> + ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> + ?typeclass_candidate:bool -> ?principal:bool -> ?hypnaming:naming_mode -> env -> evar_map -> types -> evar_map * EConstr.t val new_pure_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> + ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> + ?typeclass_candidate:bool -> ?principal:bool -> named_context_val -> evar_map -> types -> evar_map * Evar.t -val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t +val new_pure_evar_full : evar_map -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) @@ -77,7 +80,8 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr as a telescope) is [sign] *) val new_evar_instance : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> - ?store:Store.t -> ?naming:intro_pattern_naming_expr -> + ?naming:intro_pattern_naming_expr -> + ?typeclass_candidate:bool -> ?principal:bool -> named_context_val -> evar_map -> types -> constr list -> evar_map * constr diff --git a/engine/evd.ml b/engine/evd.ml index eafdc4cb46..3a77a2b440 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -144,8 +144,7 @@ type evar_info = { evar_body : evar_body; evar_filter : Filter.t; evar_source : Evar_kinds.t Loc.located; - evar_candidates : constr list option; (* if not None, list of allowed instances *) - evar_extra : Store.t } + evar_candidates : constr list option; (* if not None, list of allowed instances *)} let make_evar hyps ccl = { evar_concl = ccl; @@ -153,9 +152,7 @@ let make_evar hyps ccl = { evar_body = Evar_empty; evar_filter = Filter.identity; evar_source = Loc.tag @@ Evar_kinds.InternalHole; - evar_candidates = None; - evar_extra = Store.empty -} + evar_candidates = None; } let instance_mismatch () = anomaly (Pp.str "Signature and its instance do not match.") @@ -413,6 +410,11 @@ end type goal_kind = ToShelve | ToGiveUp +type evar_flags = + { obligation_evars : Evar.Set.t; + restricted_evars : Evar.t Evar.Map.t; + typeclass_evars : Evar.Set.t } + type evar_map = { (** Existential variables *) defn_evars : evar_info EvMap.t; @@ -425,6 +427,7 @@ type evar_map = { last_mods : Evar.Set.t; (** Metas *) metas : clbinding Metamap.t; + evar_flags : evar_flags; (** Interactive proofs *) effects : Safe_typing.private_constants; future_goals : Evar.t list; (** list of newly created evars, to be @@ -441,20 +444,82 @@ type evar_map = { extras : Store.t; } +let get_is_maybe_typeclass, (is_maybe_typeclass_hook : (evar_map -> constr -> bool) Hook.t) = Hook.make ~default:(fun evd c -> false) () + +let is_maybe_typeclass sigma c = Hook.get get_is_maybe_typeclass sigma c + (*** Lifting primitive from Evar.Map. ***) let rename evk id evd = { evd with evar_names = EvNames.rename evk id evd.evar_names } -let add_with_name ?name d e i = match i.evar_body with +let add_with_name ?name ?(typeclass_candidate = true) d e i = match i.evar_body with | Evar_empty -> let evar_names = EvNames.add_name_undefined name e i d.evar_names in - { d with undf_evars = EvMap.add e i d.undf_evars; evar_names } + let evar_flags = + if typeclass_candidate && is_maybe_typeclass d i.evar_concl then + let flags = d.evar_flags in + { flags with typeclass_evars = Evar.Set.add e flags.typeclass_evars } + else d.evar_flags + in + { d with undf_evars = EvMap.add e i d.undf_evars; evar_names; evar_flags } | Evar_defined _ -> let evar_names = EvNames.remove_name_defined e d.evar_names in { d with defn_evars = EvMap.add e i d.defn_evars; evar_names } -let add d e i = add_with_name d e i +(** Evd.add is a low-level function mainly used to update the evar_info + associated to an evar, so we prevent registering its typeclass status. *) +let add d e i = add_with_name ~typeclass_candidate:false d e i + +(*** Evar flags: typeclasses, restricted or obligation flag *) + +let get_typeclass_evars evd = evd.evar_flags.typeclass_evars + +let set_typeclass_evars evd tcs = + let flags = evd.evar_flags in + { evd with evar_flags = { flags with typeclass_evars = tcs } } + +let is_typeclass_evar evd evk = + let flags = evd.evar_flags in + Evar.Set.mem evk flags.typeclass_evars + +let set_obligation_evar evd evk = + let flags = evd.evar_flags in + let evar_flags = { flags with obligation_evars = Evar.Set.add evk flags.obligation_evars } in + { evd with evar_flags } + +let is_obligation_evar evd evk = + let flags = evd.evar_flags in + Evar.Set.mem evk flags.obligation_evars + +(** Inheritance of flags: for evar-evar and restriction cases *) + +let inherit_evar_flags evar_flags evk evk' = + let evk_typeclass = Evar.Set.mem evk evar_flags.typeclass_evars in + let evk_obligation = Evar.Set.mem evk evar_flags.obligation_evars in + if not (evk_obligation || evk_typeclass) then evar_flags + else + let typeclass_evars = + if evk_typeclass then + let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in + Evar.Set.add evk' typeclass_evars + else evar_flags.typeclass_evars + in + let obligation_evars = + if evk_obligation then + let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in + Evar.Set.add evk' obligation_evars + else evar_flags.obligation_evars + in + { evar_flags with obligation_evars; typeclass_evars } + +(** Removal: in all other cases of definition *) + +let remove_evar_flags evk evar_flags = + { typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars; + obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars; + (** Restriction information is kept. *) + restricted_evars = evar_flags.restricted_evars } (** New evars *) @@ -464,9 +529,9 @@ let evar_counter_summary_name = "evar counter" let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name let new_untyped_evar () = incr evar_ctr; Evar.unsafe_of_int !evar_ctr -let new_evar evd ?name evi = +let new_evar evd ?name ?typeclass_candidate evi = let evk = new_untyped_evar () in - let evd = add_with_name evd ?name evk evi in + let evd = add_with_name evd ?name ?typeclass_candidate evk evi in (evd, evk) let remove d e = @@ -478,7 +543,9 @@ let remove d e = in let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in let future_goals_status = EvMap.remove e d.future_goals_status in - { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status } + let evar_flags = remove_evar_flags e d.evar_flags in + { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status; + evar_flags } let find d e = try EvMap.find e d.undf_evars @@ -583,12 +650,18 @@ let cmap f evd = let create_evar_defs sigma = { sigma with conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty } +let empty_evar_flags = + { obligation_evars = Evar.Set.empty; + restricted_evars = Evar.Map.empty; + typeclass_evars = Evar.Set.empty } + let empty = { defn_evars = EvMap.empty; undf_evars = EvMap.empty; universes = UState.empty; conv_pbs = []; last_mods = Evar.Set.empty; + evar_flags = empty_evar_flags; metas = Metamap.empty; effects = Safe_typing.empty_private_constants; evar_names = EvNames.empty; (* id<->key for undefined evars *) @@ -634,9 +707,7 @@ let evar_source evk d = (find d evk).evar_source let evar_ident evk evd = EvNames.ident evk evd.evar_names let evar_key id evd = EvNames.key id evd.evar_names -let restricted = Store.field () - -let define_aux ?dorestrict def undef evk body = +let define_aux def undef evk body = let oldinfo = try EvMap.find evk undef with Not_found -> @@ -646,24 +717,39 @@ let define_aux ?dorestrict def undef evk body = anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.") in let () = assert (oldinfo.evar_body == Evar_empty) in - let evar_extra = match dorestrict with - | Some evk' -> Store.set oldinfo.evar_extra restricted evk' - | None -> oldinfo.evar_extra in - let newinfo = { oldinfo with evar_body = Evar_defined body; evar_extra } in + let newinfo = { oldinfo with evar_body = Evar_defined body } in EvMap.add evk newinfo def, EvMap.remove evk undef (* define the existential of section path sp as the constr body *) -let define evk body evd = +let define_gen evk body evd evar_flags = let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in let last_mods = match evd.conv_pbs with | [] -> evd.last_mods | _ -> Evar.Set.add evk evd.last_mods in let evar_names = EvNames.remove_name_defined evk evd.evar_names in - { evd with defn_evars; undf_evars; last_mods; evar_names } + { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags } -let is_restricted_evar evi = - Store.get evi.evar_extra restricted +(** By default, the obligation and evar tag of the evar is removed *) +let define evk body evd = + let evar_flags = remove_evar_flags evk evd.evar_flags in + define_gen evk body evd evar_flags + +(** In case of an evar-evar solution, the flags are inherited *) +let define_with_evar evk body evd = + let evk' = fst (destEvar body) in + let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in + define_gen evk body evd evar_flags + +let is_restricted_evar evd evk = + try Some (Evar.Map.find evk evd.evar_flags.restricted_evars) + with Not_found -> None + +let declare_restricted_evar evar_flags evk evk' = + { evar_flags with restricted_evars = Evar.Map.add evk evk' evar_flags.restricted_evars } + +(* In case of restriction, we declare the restriction and inherit the obligation + and typeclass flags. *) let restrict evk filter ?candidates ?src evd = let evk' = new_untyped_evar () in @@ -679,9 +765,11 @@ let restrict evk filter ?candidates ?src evd = let ctxt = Filter.filter_list filter (evar_context evar_info) in let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in let body = mkEvar(evk',id_inst) in - let (defn_evars, undf_evars) = define_aux ~dorestrict:evk' evd.defn_evars evd.undf_evars evk body in + let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in + let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in + let evar_flags = inherit_evar_flags evar_flags evk evk' in { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; - defn_evars; last_mods; evar_names }, evk' + defn_evars; last_mods; evar_names; evar_flags }, evk' let downcast evk ccl evd = let evar_info = EvMap.find evk evd.undf_evars in @@ -1019,6 +1107,7 @@ let set_metas evd metas = { universes = evd.universes; conv_pbs = evd.conv_pbs; last_mods = evd.last_mods; + evar_flags = evd.evar_flags; metas; effects = evd.effects; evar_names = evd.evar_names; diff --git a/engine/evd.mli b/engine/evd.mli index 1a5614988d..b0e3c2b869 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -83,10 +83,6 @@ type evar_body = | Evar_empty | Evar_defined of econstr - -module Store : Store.S -(** Datatype used to store additional information in evar maps. *) - type evar_info = { evar_concl : econstr; (** Type of the evar. *) @@ -102,8 +98,6 @@ type evar_info = { (** Information about the evar. *) evar_candidates : econstr list option; (** List of possible solutions when known that it is a finite list *) - evar_extra : Store.t - (** Extra store, used for clever hacks. *) } val make_evar : named_context_val -> etypes -> evar_info @@ -145,7 +139,7 @@ val has_undefined : evar_map -> bool there are uninstantiated evars in [sigma]. *) val new_evar : evar_map -> - ?name:Id.t -> evar_info -> evar_map * Evar.t + ?name:Id.t -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t (** Creates a fresh evar mapping to the given information. *) val add : evar_map -> Evar.t -> evar_info -> evar_map @@ -182,7 +176,7 @@ val raw_map_undefined : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_m (** Same as {!raw_map}, but restricted to undefined evars. For efficiency reasons. *) -val define : Evar.t-> econstr -> evar_map -> evar_map +val define : Evar.t -> econstr -> evar_map -> evar_map (** Set the body of an evar to the given constr. It is expected that: {ul {- The evar is already present in the evarmap.} @@ -190,6 +184,10 @@ val define : Evar.t-> econstr -> evar_map -> evar_map {- All the evars present in the constr should be present in the evar map.} } *) +val define_with_evar : Evar.t -> econstr -> evar_map -> evar_map +(** Same as [define ev body evd], except the body must be an existential variable [ev']. + This additionally makes [ev'] inherit the [obligation] and [typeclass] flags of [ev]. *) + val cmap : (econstr -> econstr) -> evar_map -> evar_map (** Map the function on all terms in the evar map. *) @@ -210,6 +208,8 @@ val undefined_map : evar_map -> evar_info Evar.Map.t val drop_all_defined : evar_map -> evar_map +val is_maybe_typeclass_hook : (evar_map -> constr -> bool) Hook.t + (** {6 Instantiating partial terms} *) exception NotInstantiatedEvar @@ -247,9 +247,27 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list -> possibly limiting the instances to a set of candidates (candidates are filtered according to the filter) *) -val is_restricted_evar : evar_info -> Evar.t option +val is_restricted_evar : evar_map -> Evar.t -> Evar.t option (** Tell if an evar comes from restriction of another evar, and if yes, which *) +val set_typeclass_evars : evar_map -> Evar.Set.t -> evar_map +(** Mark the given set of evars as available for resolution. + + Precondition: they should indeed refer to undefined typeclass evars. + *) + +val get_typeclass_evars : evar_map -> Evar.Set.t +(** The set of undefined typeclass evars *) + +val is_typeclass_evar : evar_map -> Evar.t -> bool +(** Is the evar declared resolvable for typeclass resolution *) + +val set_obligation_evar : evar_map -> Evar.t -> evar_map +(** Declare an evar as an obligation *) + +val is_obligation_evar : evar_map -> Evar.t -> bool +(** Is the evar declared as an obligation *) + val downcast : Evar.t-> etypes -> evar_map -> evar_map (** Change the type of an undefined evar to a new type assumed to be a subtype of its current type; subtyping must be ensured by caller *) @@ -357,6 +375,9 @@ val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map *) +module Store : Store.S +(** Datatype used to store additional information in evar maps. *) + val get_extra_data : evar_map -> Store.t val set_extra_data : Store.t -> evar_map -> evar_map diff --git a/engine/proofview.ml b/engine/proofview.ml index 12d31e5f46..304b2dff84 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -60,19 +60,14 @@ type telescope = | TNil of Evd.evar_map | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope) -let typeclass_resolvable = Evd.Store.field () - let dependent_init = - (* Goals are created with a store which marks them as unresolvable - for type classes. *) - let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () in (* Goals don't have a source location. *) let src = Loc.tag @@ Evar_kinds.GoalEvar in (* Main routine *) let rec aux = function | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } | TCons (env, sigma, typ, t) -> - let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~store typ in + let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~typeclass_candidate:false typ in let (gl, _) = EConstr.destEvar sigma econstr in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let entry = (econstr, typ) :: ret in @@ -745,26 +740,28 @@ let unshelve l p = let l = undefined p.solution l in { p with comb = p.comb@l } -let mark_in_evm ~goal evd content = - let info = Evd.find evd content in - let info = +let mark_in_evm ~goal evd evars = + let evd = if goal then - { info with Evd.evar_source = match info.Evd.evar_source with - (* Two kinds for goal evars: - - GoalEvar (morally not dependent) - - VarInstance (morally dependent of some name). - This is a heuristic for naming these evars. *) - | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} | - Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id - | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x - | loc,_ -> loc,Evar_kinds.GoalEvar } - else info - in - let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with - | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () } - | Some () -> info + let mark evd content = + let info = Evd.find evd content in + let info = + { info with Evd.evar_source = match info.Evd.evar_source with + (* Two kinds for goal evars: + - GoalEvar (morally not dependent) + - VarInstance (morally dependent of some name). + This is a heuristic for naming these evars. *) + | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} | + Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id + | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x + | loc,_ -> loc,Evar_kinds.GoalEvar } + in Evd.add evd content info + in CList.fold_left mark evd evars + else evd in - Evd.add evd content info + let tcs = Evd.get_typeclass_evars evd in + let evset = Evar.Set.of_list evars in + Evd.set_typeclass_evars evd (Evar.Set.diff tcs evset) let with_shelf tac = let open Proof in @@ -781,7 +778,7 @@ let with_shelf tac = let sigma = Evd.restore_future_goals sigma fgoals in (* Ensure we mark and return only unsolved goals *) let gls' = undefined_evars sigma (CList.rev_append gls' gls) in - let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in + let sigma = mark_in_evm ~goal:false sigma gls' in let npv = { npv with shelf; solution = sigma } in Pv.set npv >> tclUNIT (gls', ans) @@ -1035,7 +1032,7 @@ module Unsafe = struct let reset_future_goals p = { p with solution = Evd.reset_future_goals p.solution } - let mark_as_goal evd content = + let mark_as_goals evd content = mark_in_evm ~goal:true evd content let advance = Evarutil.advance @@ -1043,9 +1040,7 @@ module Unsafe = struct let undefined = undefined let mark_as_unresolvable p gl = - { p with solution = mark_in_evm ~goal:false p.solution gl } - - let typeclass_resolvable = typeclass_resolvable + { p with solution = mark_in_evm ~goal:false p.solution [gl] } end @@ -1065,10 +1060,6 @@ let goal_nf_evar sigma gl = let sigma = Evd.add sigma gl evi in (gl, sigma) -let goal_extra evars gl = - let evi = Evd.find evars gl in - evi.Evd.evar_extra - let catchable_exception = function | Logic_monad.Exception _ -> false @@ -1093,7 +1084,6 @@ module Goal = struct let sigma {sigma} = sigma let hyps {env} = EConstr.named_context env let concl {concl} = concl - let extra {sigma; self} = goal_extra sigma self let gmake_with info env sigma goal state = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; diff --git a/engine/proofview.mli b/engine/proofview.mli index 0bb3229a9b..cda4808a23 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -456,9 +456,9 @@ module Unsafe : sig (** Clears the future goals store in the proof view. *) val reset_future_goals : proofview -> proofview - (** Give an evar the status of a goal (changes its source location - and makes it unresolvable for type classes. *) - val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map + (** Give the evars the status of a goal (changes their source location + and makes them unresolvable for type classes. *) + val mark_as_goals : Evd.evar_map -> Evar.t list -> Evd.evar_map (** Make an evar unresolvable for type classes. *) val mark_as_unresolvable : proofview -> Evar.t -> proofview @@ -475,8 +475,6 @@ module Unsafe : sig val undefined : Evd.evar_map -> Proofview_monad.goal_with_state list -> Proofview_monad.goal_with_state list - val typeclass_resolvable : unit Evd.Store.field - end (** This module gives access to the innards of the monad. Its use is @@ -507,7 +505,6 @@ module Goal : sig val hyps : t -> named_context val env : t -> Environ.env val sigma : t -> Evd.evar_map - val extra : t -> Evd.Store.t val state : t -> Proofview_monad.StateStore.t (** [nf_enter t] applies the goal-dependent tactic [t] in each goal diff --git a/engine/termops.ml b/engine/termops.ml index e1f5fb0d7f..5e220fd8f1 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -365,12 +365,18 @@ let pr_evar_map_gen with_univs pr_evars sigma = else str "CONSTRAINTS:" ++ brk (0, 1) ++ pr_evar_constraints sigma conv_pbs ++ fnl () + and typeclasses = + let evars = Evd.get_typeclass_evars sigma in + if Evar.Set.is_empty evars then mt () + else + str "TYPECLASSES:" ++ brk (0, 1) ++ + prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl () and metas = if List.is_empty (Evd.meta_list sigma) then mt () else str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma in - evs ++ svs ++ cstrs ++ metas + evs ++ svs ++ cstrs ++ typeclasses ++ metas let pr_evar_list sigma l = let open Evd in diff --git a/interp/discharge.ml b/interp/discharge.ml index 0e44a8b467..21b2e85e8f 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Names -open CErrors open Util open Term open Constr @@ -17,17 +15,10 @@ open Vars open Declarations open Cooking open Entries -open Context.Rel.Declaration (********************************) (* Discharging mutual inductive *) -let detype_param = - function - | LocalAssum (Name id, p) -> id, LocalAssumEntry p - | LocalDef (Name id, p,_) -> id, LocalDefEntry p - | _ -> anomaly (Pp.str "Unnamed inductive local variable.") - (* Replace Var(y1)..Var(yq):C1..Cq |- Ij:Bj @@ -57,7 +48,7 @@ let abstract_inductive decls nparamdecls inds = (* To be sure to be the same as before, should probably be moved to process_inductive *) let params' = let (_,arity,_,_,_) = List.hd inds' in let (params,_) = decompose_prod_n_assum nparamdecls' arity in - List.map detype_param params + params in let ind'' = List.map diff --git a/kernel/entries.ml b/kernel/entries.ml index 94248ad26b..c5bcd74072 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -16,14 +16,6 @@ open Constr constants/axioms, mutual inductive definitions, modules and module types *) - -(** {6 Local entries } *) - -type local_entry = - | LocalDefEntry of constr - | LocalAssumEntry of constr - - (** {6 Declaration of inductive types. } *) (** Assume the following definition in concrete syntax: @@ -54,7 +46,7 @@ type mutual_inductive_entry = { record in their respective projections. Not used by the kernel. Some None: non-primitive record *) mind_entry_finite : Declarations.recursivity_kind; - mind_entry_params : (Id.t * local_entry) list; + mind_entry_params : Constr.rel_context; mind_entry_inds : one_inductive_entry list; mind_entry_universes : inductive_universes; (* universe constraints and the constraints for subtyping of diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b976469ff7..0346026aa4 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -271,7 +271,8 @@ let typecheck_inductive env mie = | Polymorphic_ind_entry ctx -> push_context ctx env | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env in - let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in + let env_params = check_context env' mie.mind_entry_params in + let paramsctxt = mie.mind_entry_params in (* We first type arity of each inductive definition *) (* This allows building the environment of arities and to share *) (* the set of constraints *) diff --git a/kernel/names.ml b/kernel/names.ml index 7cd749de1d..18560d5f8d 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -872,6 +872,8 @@ struct let equal (c, b) (c', b') = Repr.equal c c' && b == b' + let repr_equal p p' = Repr.equal (repr p) (repr p') + let hash (c, b) = (if b then 0 else 1) + Repr.hash c module SyntacticOrd = struct diff --git a/kernel/names.mli b/kernel/names.mli index 37930c12e2..98995752a2 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -608,6 +608,9 @@ module Projection : sig val hcons : t -> t (** Hashconsing of projections. *) + val repr_equal : t -> t -> bool + (** Ignoring the unfolding boolean. *) + val compare : t -> t -> int val map : (MutInd.t -> MutInd.t) -> t -> t diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 3481d3bedb..1bb2d3c79c 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -515,25 +515,19 @@ let infer_v env cv = (* Typing of several terms. *) -let infer_local_decl env id = function - | Entries.LocalDefEntry c -> - let () = check_wellformed_universes env c in - let t = execute env c in - RelDecl.LocalDef (Name id, c, t) - | Entries.LocalAssumEntry c -> - let () = check_wellformed_universes env c in - let t = execute env c in - RelDecl.LocalAssum (Name id, check_assumption env c t) - -let infer_local_decls env decls = - let rec inferec env = function - | (id, d) :: l -> - let (env, l) = inferec env l in - let d = infer_local_decl env id d in - (push_rel d env, Context.Rel.add d l) - | [] -> (env, Context.Rel.empty) - in - inferec env decls +let check_context env rels = + let open Context.Rel.Declaration in + Context.Rel.fold_outside (fun d env -> + match d with + | LocalAssum (_,ty) -> + let _ = infer_type env ty in + push_rel d env + | LocalDef (_,bd,ty) -> + let j1 = infer env bd in + let _ = infer_type env ty in + conv_leq false env j1.uj_type ty; + push_rel d env) + rels ~init:env let judge_of_prop = make_judge mkProp type1 let judge_of_set = make_judge mkSet type1 diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 1fd070d9d5..d24002065b 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -12,7 +12,6 @@ open Names open Constr open Univ open Environ -open Entries (** {6 Typing functions (not yet tagged as safe) } @@ -27,8 +26,8 @@ val infer : env -> constr -> unsafe_judgment val infer_v : env -> constr array -> unsafe_judgment array val infer_type : env -> types -> unsafe_type_judgment -val infer_local_decls : - env -> (Id.t * local_entry) list -> (env * Constr.rel_context) +val check_context : + env -> Constr.rel_context -> env (** {6 Basic operations of the typing machine. } *) diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml index c2bcd73fff..d0b01453a0 100644 --- a/lib/coqProject_file.ml +++ b/lib/coqProject_file.ml @@ -29,6 +29,7 @@ type project = { v_files : string sourced list; mli_files : string sourced list; ml4_files : string sourced list; + mlg_files : string sourced list; ml_files : string sourced list; mllib_files : string sourced list; mlpack_files : string sourced list; @@ -66,6 +67,7 @@ let mk_project project_file makefile install_kind use_ocamlopt = { v_files = []; mli_files = []; ml4_files = []; + mlg_files = []; ml_files = []; mllib_files = []; mlpack_files = []; @@ -223,6 +225,7 @@ let process_cmd_line orig_dir proj args = { proj with v_files = proj.v_files @ [sourced f] } | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] } | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] } + | ".mlg" -> { proj with mlg_files = proj.mlg_files @ [sourced f] } | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] } | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] } | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced f] } @@ -249,9 +252,9 @@ let rec find_project_file ~from ~projfile_name = else find_project_file ~from:newdir ~projfile_name ;; -let all_files { v_files; ml_files; mli_files; ml4_files; +let all_files { v_files; ml_files; mli_files; ml4_files; mlg_files; mllib_files; mlpack_files } = - v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files + v_files @ mli_files @ ml4_files @ mlg_files @ ml_files @ mllib_files @ mlpack_files let map_sourced_list f l = List.map (fun x -> f x.thing) l ;; diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 5780bb5d78..2a6a09a9a0 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -23,6 +23,7 @@ type project = { v_files : string sourced list; mli_files : string sourced list; ml4_files : string sourced list; + mlg_files : string sourced list; ml_files : string sourced list; mllib_files : string sourced list; mlpack_files : string sourced list; diff --git a/library/coqlib.ml b/library/coqlib.ml index a044a9a395..784360dc8a 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -227,8 +227,7 @@ type coq_eq_data = { (* Leibniz equality on Type *) -let build_eqdata_gen lib str = - let _ = check_required_library lib in { +let build_eqdata_gen str = { eq = lib_ref ("core." ^ str ^ ".type"); ind = lib_ref ("core." ^ str ^ ".ind"); refl = lib_ref ("core." ^ str ^ ".refl"); @@ -237,9 +236,9 @@ let build_eqdata_gen lib str = congr = lib_ref ("core." ^ str ^ ".congr"); } -let build_coq_eq_data () = build_eqdata_gen logic_module_name "eq" -let build_coq_jmeq_data () = build_eqdata_gen jmeq_module_name "JMeq" -let build_coq_identity_data () = build_eqdata_gen datatypes_module_name "identity" +let build_coq_eq_data () = build_eqdata_gen "eq" +let build_coq_jmeq_data () = build_eqdata_gen "JMeq" +let build_coq_identity_data () = build_eqdata_gen "identity" (* Inversion data... *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 9dd98a4ab7..9f7669f1d5 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -89,8 +89,8 @@ let goalevars evars = fst evars let cstrevars evars = snd evars let new_cstr_evar (evd,cstrs) env t = - let s = Typeclasses.set_resolvable Evd.Store.empty false in - let (evd', t) = Evarutil.new_evar ~store:s env evd t in + (** We handle the typeclass resolution of constraints ourselves *) + let (evd', t) = Evarutil.new_evar env evd ~typeclass_candidate:false t in let ev, _ = destEvar evd' t in (evd', Evar.Set.add ev cstrs), t @@ -632,9 +632,6 @@ let solve_remaining_by env sigma holes by = let no_constraints cstrs = fun ev _ -> not (Evar.Set.mem ev cstrs) -let all_constraints cstrs = - fun ev _ -> Evar.Set.mem ev cstrs - let poly_inverse sort = if sort then PropGlobal.inverse else TypeGlobal.inverse @@ -1453,10 +1450,11 @@ let apply_strategy (s : strategy) env unfresh concl (prop, cstr) evars = res let solve_constraints env (evars,cstrs) = - let filter = all_constraints cstrs in - Typeclasses.resolve_typeclasses env ~filter ~split:false ~fail:true - (Typeclasses.mark_resolvables ~filter evars) - + let oldtcs = Evd.get_typeclass_evars evars in + let evars' = Evd.set_typeclass_evars evars cstrs in + let evars' = Typeclasses.resolve_typeclasses env ~filter:all_evars ~split:false ~fail:true evars' in + Evd.set_typeclass_evars evars' oldtcs + let nf_zeta = Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 8dbef47fe1..a2dce621d9 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -164,7 +164,7 @@ let ltac_call tac (args:glob_tactic_arg list) = let dummy_goal env sigma = let (gl,_,sigma) = - Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in + Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp in {Evd.it = gl; Evd.sigma = sigma} let constr_of evd v = match Value.to_constr v with diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 6746eff223..a284c3bfc7 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -730,13 +730,10 @@ let pf_abs_prod name gl c cl = pf_mkprod gl c ~name (Termops.subst_term (project (** look up a name in the ssreflect internals module *) let ssrdirpath = DirPath.make [Id.of_string "ssreflect"] let ssrqid name = Libnames.make_qualid ssrdirpath (Id.of_string name) -let ssrtopqid name = Libnames.qualid_of_ident (Id.of_string name) -let locate_reference qid = - Smartlocate.global_of_extended_global (Nametab.locate_extended qid) let mkSsrRef name = - try locate_reference (ssrqid name) with Not_found -> - try locate_reference (ssrtopqid name) with Not_found -> - CErrors.user_err (Pp.str "Small scale reflection library not loaded") + let qn = Format.sprintf "plugins.ssreflect.%s" name in + if Coqlib.has_ref qn then Coqlib.lib_ref qn else + CErrors.user_err Pp.(str "Small scale reflection library not loaded (" ++ str name ++ str ")") let mkSsrRRef name = (DAst.make @@ GRef (mkSsrRef name,None)), None let mkSsrConst name env sigma = EConstr.fresh_global env sigma (mkSsrRef name) @@ -1365,7 +1362,7 @@ let tacTYPEOF c = Goal.enter_one ~__LOC__ (fun g -> (** This tactic creates a partial proof realizing the introduction rule, but does not check anything. *) -let unsafe_intro env store decl b = +let unsafe_intro env decl b = let open Context.Named.Declaration in Refine.refine ~typecheck:false begin fun sigma -> let ctx = Environ.named_context_val env in @@ -1374,7 +1371,7 @@ let unsafe_intro env store decl b = let ninst = EConstr.mkRel 1 :: inst in let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in let sigma, ev = - Evarutil.new_evar_instance nctx sigma nb ~principal:true ~store ninst in + Evarutil.new_evar_instance nctx sigma nb ~principal:true ninst in sigma, EConstr.mkNamedLambda_or_LetIn decl ev end @@ -1418,7 +1415,7 @@ let-in even after reduction, it fails. In case of success, the original name and final id are passed to the continuation [k] which gets evaluated. *) let tclINTRO ~id ~conclusion:k = Goal.enter begin fun gl -> let open Context in - let env, sigma, extra, g = Goal.(env gl, sigma gl, extra gl, concl gl) in + let env, sigma, g = Goal.(env gl, sigma gl, concl gl) in let decl, t, no_red = decompose_assum env sigma g in let original_name = Rel.Declaration.get_name decl in let already_used = Tacmach.New.pf_ids_of_hyps gl in @@ -1433,7 +1430,7 @@ let tclINTRO ~id ~conclusion:k = Goal.enter begin fun gl -> in if List.mem id already_used then errorstrm Pp.(Id.print id ++ str" already used"); - unsafe_intro env extra (set_decl_id id decl) t <*> + unsafe_intro env (set_decl_id id decl) t <*> (if no_red then tclUNIT () else tclFULL_BETAIOTA) <*> k ~orig_name:original_name ~new_name:id end diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 9ba23467e7..566a933522 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -212,8 +212,7 @@ val pf_abs_prod : EConstr.t -> Goal.goal Evd.sigma * EConstr.types val mkSsrRRef : string -> Glob_term.glob_constr * 'a option -val mkSsrRef : string -> GlobRef.t -val mkSsrConst : +val mkSsrConst : string -> env -> evar_map -> evar_map * EConstr.t val pf_mkSsrConst : diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 460bdc6d23..e43cab094b 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -159,6 +159,10 @@ Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) := Notation "<hidden n >" := (abstract _ n _). Notation "T (* n *)" := (abstract T n abstract_key). +Register abstract_lock as plugins.ssreflect.abstract_lock. +Register abstract_key as plugins.ssreflect.abstract_key. +Register abstract as plugins.ssreflect.abstract. + (* Constants for tactic-views *) Inductive external_view : Type := tactic_view of Type. @@ -287,6 +291,8 @@ Variant phant (p : Type) := Phant. Definition protect_term (A : Type) (x : A) : A := x. +Register protect_term as plugins.ssreflect.protect_term. + (* The ssreflect idiom for a non-keyed pattern: *) (* - unkeyed t wiil match any subterm that unifies with t, regardless of *) (* whether it displays the same head symbol as t. *) @@ -336,6 +342,9 @@ Notation nosimpl t := (let: tt := tt in t). Lemma master_key : unit. Proof. exact tt. Qed. Definition locked A := let: tt := master_key in fun x : A => x. +Register master_key as plugins.ssreflect.master_key. +Register locked as plugins.ssreflect.locked. + Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed. (* Needed for locked predicates, in particular for eqType's. *) @@ -395,12 +404,18 @@ Definition ssr_have_let Pgoal Plemma step (rest : let x : Plemma := step in Pgoal) : Pgoal := rest. Arguments ssr_have_let [Pgoal]. +Register ssr_have as plugins.ssreflect.ssr_have. +Register ssr_have_let as plugins.ssreflect.ssr_have_let. + Definition ssr_suff Plemma Pgoal step (rest : Plemma) : Pgoal := step rest. Arguments ssr_suff Plemma [Pgoal]. Definition ssr_wlog := ssr_suff. Arguments ssr_wlog Plemma [Pgoal]. +Register ssr_suff as plugins.ssreflect.ssr_suff. +Register ssr_wlog as plugins.ssreflect.ssr_wlog. + (* Internal N-ary congruence lemmas for the congr tactic. *) Fixpoint nary_congruence_statement (n : nat) @@ -425,6 +440,9 @@ Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal. Proof. by move->. Qed. Arguments ssr_congr_arrow : clear implicits. +Register nary_congruence as plugins.ssreflect.nary_congruence. +Register ssr_congr_arrow as plugins.ssreflect.ssr_congr_arrow. + (* View lemmas that don't use reflection. *) Section ApplyIff. diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 7f9a9e125e..5067d8af31 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -16,7 +16,6 @@ open Printer open Term open Constr open Termops -open Globnames open Tactypes open Tacmach @@ -98,6 +97,11 @@ let subgoals_tys sigma (relctx, concl) = * generalize the equality in case eqid is not None * 4. build the tactic handle intructions and clears as required in ipats and * by eqid *) + +let get_eq_type gl = + let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in + gl, EConstr.of_constr eq + let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac gl = (* some sanity checks *) let oc, orig_clr, occ, c_gen, gl = match what with @@ -115,8 +119,6 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in ppdebug(lazy(Pp.str(if is_case then "==CASE==" else "==ELIM=="))); let fire_subst gl t = Reductionops.nf_evar (project gl) t in - let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in - let eq = EConstr.of_constr eq in let is_undef_pat = function | sigma, T t -> EConstr.isEvar sigma (EConstr.of_constr t) | _ -> false in @@ -322,6 +324,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let k = List.length deps in let c = fire_subst gl (List.assoc (n_elim_args - k - 1) elim_args) in let gl, t = pfe_type_of gl c in + let gl, eq = get_eq_type gl in let gen_eq_tac, gl = let refl = EConstr.mkApp (eq, [|t; c; c|]) in let new_concl = EConstr.mkArrow refl (EConstr.Vars.lift 1 (pf_concl orig_gl)) in @@ -421,7 +424,7 @@ let injectl2rtac sigma c = match EConstr.kind sigma c with let is_injection_case c gl = let gl, cty = pfe_type_of gl c in let (mind,_), _ = pf_reduce_to_quantified_ind gl cty in - GlobRef.equal (IndRef mind) Coqlib.(lib_ref "core.eq.type") + Coqlib.check_ind_ref "core.eq.type" mind let perform_injection c gl = let gl, cty = pfe_type_of gl c in diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 4a63dd4708..7f67487f5d 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -356,8 +356,10 @@ let nf_open_term sigma0 ise c = let unif_end env sigma0 ise0 pt ok = let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in + let tcs = Evd.get_typeclass_evars ise in let s, uc, t = nf_open_term sigma0 ise pt in let ise1 = create_evar_defs s in + let ise1 = Evd.set_typeclass_evars ise1 (Evar.Set.filter (fun ev -> Evd.is_undefined ise1 ev) tcs) in let ise1 = Evd.set_universe_context ise1 uc in let ise2 = Typeclasses.resolve_typeclasses ~fail:true env ise1 in if not (ok ise) then raise NoProgress else @@ -1045,7 +1047,7 @@ let thin id sigma goal = match ans with | None -> sigma | Some (sigma, hyps, concl) -> - let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in + let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl in let sigma = Goal.V82.partial_solution_to sigma goal gl ev in sigma diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 54e847988b..164f5ab96d 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -296,8 +296,7 @@ let inductive_template env sigma tmloc ind = let ty = EConstr.of_constr ty in let ty' = substl subst ty in let sigma, e = - Evarutil.new_evar env ~src:(hole_source n) - sigma ty' + Evarutil.new_evar env ~src:(hole_source n) ~typeclass_candidate:false sigma ty' in (sigma, e::subst,e::evarl,n+1) | LocalDef (na,b,ty) -> @@ -1698,7 +1697,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context !!env) in - let sigma, ev' = Evarutil.new_evar ~src !!env sigma ty in + let sigma, ev' = Evarutil.new_evar ~src ~typeclass_candidate:false !!env sigma ty in begin match solve_simple_eqn (evar_conv_x full_transparent_state) !!env sigma (None,ev,substl inst ev') with | Success evd -> evdref := evd | UnifFailure _ -> assert false @@ -1734,7 +1733,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = (named_context !!extenv) in let filter = Filter.make (rel_filter @ named_filter) in let candidates = List.rev (u :: List.map mkRel vl) in - let sigma, ev = Evarutil.new_evar !!extenv ~src ~filter ~candidates sigma ty in + let sigma, ev = Evarutil.new_evar !!extenv ~src ~filter ~candidates ~typeclass_candidate:false sigma ty in let () = evdref := sigma in lift k ev in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f0ff1aa93b..6a75be352b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -711,8 +711,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in ise_try evd [f1; f2] - | Proj (p, c), Proj (p', c') - when Constant.equal (Projection.constant p) (Projection.constant p') -> + | Proj (p, c), Proj (p', c') when Projection.repr_equal p p' -> let f1 i = ise_and i [(fun i -> evar_conv_x ts env i CONV c c'); diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 22f438c00c..674f6846ae 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1238,33 +1238,31 @@ let check_evar_instance evd evk1 body conv_algo = | Success evd -> evd | UnifFailure _ -> raise (IllTypedInstance (evenv,ty, evi.evar_concl)) -let update_evar_source ev1 ev2 evd = +let update_evar_info ev1 ev2 evd = + (* We update the source of obligation evars during evar-evar unifications. *) let loc, evs2 = evar_source ev2 evd in - match evs2 with - | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) -> - let evi = Evd.find evd ev1 in - Evd.add evd ev1 {evi with evar_source = loc, evs2} - | _ -> evd - + let evi = Evd.find evd ev1 in + Evd.add evd ev1 {evi with evar_source = loc, evs2} + let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) = try let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in - let evd' = Evd.define evk2 body evd in - let evd' = update_evar_source (fst (destEvar evd body)) evk2 evd' in - check_evar_instance evd' evk2 body g + let evd' = Evd.define_with_evar evk2 body evd in + let evd' = + if is_obligation_evar evd evk2 then + update_evar_info evk2 (fst (destEvar evd' body)) evd' + else evd' + in + check_evar_instance evd' evk2 body g with EvarSolvedOnTheFly (evd,c) -> f env evd pbty ev2 c let opp_problem = function None -> None | Some b -> Some (not b) let preferred_orientation evd evk1 evk2 = - let _,src1 = (Evd.find_undefined evd evk1).evar_source in - let _,src2 = (Evd.find_undefined evd evk2).evar_source in - (* This is a heuristic useful for program to work *) - match src1,src2 with - | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) , _ -> true - | _, (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) -> false - | _ -> true + if is_obligation_evar evd evk1 then true + else if is_obligation_evar evd evk2 then false + else true let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let aliases = make_alias_map env evd in diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index a56a8314e6..422a05c19a 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -196,7 +196,7 @@ let infer_inductive env mie = Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances) LMap.empty uarray in - let env, _ = Typeops.infer_local_decls env params in + let env = Typeops.check_context env params in let variances = List.fold_left (fun variances entry -> let variances = infer_arity_constructor true env variances entry.mind_entry_arity diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f2881e4a19..37afcf75e1 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -510,6 +510,15 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma | Some ty -> sigma, ty | None -> new_type_evar env sigma loc in let sigma, uj_val = new_evar env sigma ~src:(loc,k) ~naming ty in + let sigma = + if Flags.is_program_mode () then + match k with + | Evar_kinds.QuestionMark _ + | Evar_kinds.ImplicitArg (_, _, false) -> + Evd.set_obligation_evar sigma (fst (destEvar sigma uj_val)) + | _ -> sigma + else sigma + in sigma, { uj_val; uj_type = ty } | GHole (k, _naming, Some arg) -> diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 5dbe95a471..367a48cb5e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -398,8 +398,7 @@ struct match x, y with | Cst_const (c1,u1), Cst_const (c2, u2) -> Constant.equal c1 c2 && Univ.Instance.equal u1 u2 - | Cst_proj p1, Cst_proj p2 -> - Constant.equal (Projection.constant p1) (Projection.constant p2) + | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2 | _, _ -> false in let rec equal_rec sk1 sk2 = diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 0bc35e5358..4aea2c3db9 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -166,6 +166,21 @@ let rec is_class_type evd c = let is_class_evar evd evi = is_class_type evd evi.Evd.evar_concl +let is_class_constr sigma c = + try let gr, u = Termops.global_of_constr sigma c in + GlobRef.Map.mem gr !classes + with Not_found -> false + +let rec is_maybe_class_type evd c = + let c, _ = Termops.decompose_app_vect evd c in + match EConstr.kind evd c with + | Prod (_, _, t) -> is_maybe_class_type evd t + | Cast (t, _, _) -> is_maybe_class_type evd t + | Evar _ -> true + | _ -> is_class_constr evd c + +let () = Hook.set Evd.is_maybe_typeclass_hook (fun evd c -> is_maybe_class_type evd (EConstr.of_constr c)) + (* * classes persistent object *) @@ -481,63 +496,29 @@ let instances r = let is_class gr = GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes -(* To embed a boolean for resolvability status. - This is essentially a hack to mark which evars correspond to - goals and do not need to be resolved when we have nested [resolve_all_evars] - calls (e.g. when doing apply in an External hint in typeclass_instances). - Would be solved by having real evars-as-goals. - - Nota: we will only check the resolvability status of undefined evars. - *) - -let resolvable = Proofview.Unsafe.typeclass_resolvable - -let set_resolvable s b = - if b then Store.remove s resolvable - else Store.set s resolvable () - -let is_resolvable evi = - assert (match evi.evar_body with Evar_empty -> true | _ -> false); - Option.is_empty (Store.get evi.evar_extra resolvable) - -let mark_resolvability_undef b evi = - if is_resolvable evi == (b : bool) then evi - else - let t = set_resolvable evi.evar_extra b in - { evi with evar_extra = t } - -let mark_resolvability b evi = - assert (match evi.evar_body with Evar_empty -> true | _ -> false); - mark_resolvability_undef b evi - -let mark_unresolvable evi = mark_resolvability false evi -let mark_resolvable evi = mark_resolvability true evi - open Evar_kinds -type evar_filter = Evar.t -> Evar_kinds.t -> bool +type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool + +let make_unresolvables filter evd = + let tcs = Evd.get_typeclass_evars evd in + Evd.set_typeclass_evars evd (Evar.Set.filter (fun x -> not (filter x)) tcs) let all_evars _ _ = true -let all_goals _ = function VarInstance _ | GoalEvar -> true | _ -> false +let all_goals _ source = + match Lazy.force source with + | VarInstance _ | GoalEvar -> true + | _ -> false + let no_goals ev evi = not (all_goals ev evi) -let no_goals_or_obligations _ = function +let no_goals_or_obligations _ source = + match Lazy.force source with | VarInstance _ | GoalEvar | QuestionMark _ -> false | _ -> true -let mark_resolvability filter b sigma = - let map ev evi = - if filter ev (snd evi.evar_source) then mark_resolvability_undef b evi - else evi - in - Evd.raw_map_undefined map sigma - -let mark_unresolvables ?(filter=all_evars) sigma = mark_resolvability filter false sigma -let mark_resolvables ?(filter=all_evars) sigma = mark_resolvability filter true sigma - let has_typeclasses filter evd = - let check ev evi = - filter ev (snd evi.evar_source) && is_resolvable evi && is_class_evar evd evi - in - Evar.Map.exists check (Evd.undefined_map evd) + let tcs = get_typeclass_evars evd in + let check ev = filter ev (lazy (snd (Evd.find evd ev).evar_source)) in + Evar.Set.exists check tcs let get_solve_all_instances, solve_all_instances_hook = Hook.make () @@ -548,7 +529,7 @@ let solve_all_instances env evd filter unique split fail = (* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *) (* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *) -let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) +let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) ?(split=true) ?(fail=true) env evd = - if fast_path && not (has_typeclasses filter evd) then evd + if not (has_typeclasses filter evd) then evd else solve_all_instances env evd filter unique split fail diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index f0437be4ed..ee9c83dad3 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -93,7 +93,7 @@ val instance_constructor : typeclass EConstr.puniverses -> EConstr.t list -> EConstr.t option * EConstr.t (** Filter which evars to consider for resolution. *) -type evar_filter = Evar.t -> Evar_kinds.t -> bool +type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool val all_evars : evar_filter val all_goals : evar_filter val no_goals : evar_filter @@ -107,16 +107,12 @@ val no_goals_or_obligations : evar_filter An unresolvable evar is an evar the type-class engine will NOT try to solve *) -val set_resolvable : Evd.Store.t -> bool -> Evd.Store.t -val is_resolvable : evar_info -> bool -val mark_unresolvable : evar_info -> evar_info -val mark_unresolvables : ?filter:evar_filter -> evar_map -> evar_map -val mark_resolvables : ?filter:evar_filter -> evar_map -> evar_map -val mark_resolvable : evar_info -> evar_info +val make_unresolvables : (Evar.t -> bool) -> evar_map -> evar_map + val is_class_evar : evar_map -> evar_info -> bool val is_class_type : evar_map -> EConstr.types -> bool -val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool -> +val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool -> ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> evar_map * EConstr.constr diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 95e908c4dd..d25ae38c53 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -324,21 +324,21 @@ let adjust_meta_source evd mv = function *) let clenv_pose_metas_as_evars clenv dep_mvs = - let rec fold clenv = function - | [] -> clenv + let rec fold clenv evs = function + | [] -> clenv, evs | mv::mvs -> let ty = clenv_meta_type clenv mv in (* Postpone the evar-ization if dependent on another meta *) (* This assumes no cycle in the dependencies - is it correct ? *) - if occur_meta clenv.evd ty then fold clenv (mvs@[mv]) + if occur_meta clenv.evd ty then fold clenv evs (mvs@[mv]) else let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in let evd = clenv.evd in let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in let clenv = clenv_assign mv evar {clenv with evd=evd} in - fold clenv mvs in - fold clenv dep_mvs + fold clenv (fst (destEvar evd evar) :: evs) mvs in + fold clenv [] dep_mvs (******************************************************************) @@ -608,8 +608,7 @@ let make_evar_clause env sigma ?len t = else match EConstr.kind sigma t with | Cast (t, _, _) -> clrec (sigma, holes) n t | Prod (na, t1, t2) -> - let store = Typeclasses.set_resolvable Evd.Store.empty false in - let (sigma, ev) = new_evar ~store env sigma t1 in + let (sigma, ev) = new_evar env sigma ~typeclass_candidate:false t1 in let dep = not (noccurn sigma 1 t2) in let hole = { hole_evar = ev; diff --git a/proofs/clenv.mli b/proofs/clenv.mli index f9506290a0..03acb9e46e 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -72,7 +72,7 @@ val clenv_unique_resolver : val clenv_dependent : clausenv -> metavariable list -val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv +val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv * Evar.t list (** {6 Bindings } *) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index ba4cde6d67..77f5804665 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -62,37 +62,19 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv = (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); clenv_pose_metas_as_evars clenv dep_mvs -(** Use our own fast path, more informative than from Typeclasses *) -let check_tc evd = - let has_resolvable = ref false in - let check _ evi = - let res = Typeclasses.is_resolvable evi in - if res then - let () = has_resolvable := true in - Typeclasses.is_class_evar evd evi - else false - in - let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in - (has_typeclass, !has_resolvable) - let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = (** ppedrot: a Goal.enter here breaks things, because the tactic below may solve goals by side effects, while the compatibility layer keeps those useless goals. That deserves a FIXME. *) Proofview.V82.tactic begin fun gl -> - let clenv = clenv_pose_dependent_evars ~with_evars clenv in + let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in let evd' = if with_classes then - let (has_typeclass, has_resolvable) = check_tc clenv.evd in let evd' = - if has_typeclass then - Typeclasses.resolve_typeclasses ~fast_path:false ~filter:Typeclasses.all_evars + Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:(not with_evars) ~split:false clenv.env clenv.evd - else clenv.evd in - if has_resolvable then - Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd' - else evd' + Typeclasses.make_unresolvables (fun x -> List.mem_f Evar.equal x evars) evd' else clenv.evd in let clenv = { clenv with evd = evd' } in @@ -101,6 +83,9 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl end +let clenv_pose_dependent_evars ?(with_evars=false) clenv = + fst (clenv_pose_dependent_evars ~with_evars clenv) + open Unification let dft = default_unify_flags diff --git a/proofs/goal.ml b/proofs/goal.ml index c14c0a8a77..4e540de538 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -50,13 +50,8 @@ module V82 = struct let evi = Evd.find evars gl in evi.Evd.evar_concl - (* Access to ".evar_extra" *) - let extra evars gl = - let evi = Evd.find evars gl in - evi.Evd.evar_extra - (* Old style mk_goal primitive *) - let mk_goal evars hyps concl extra = + let mk_goal evars hyps concl = (* A goal created that way will not be used by refine and will not be shelved. It must not appear as a future_goal, so the future goals are restored to their initial value after the evar is @@ -67,11 +62,9 @@ module V82 = struct Evd.evar_filter = Evd.Filter.identity; Evd.evar_body = Evd.Evar_empty; Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar); - Evd.evar_candidates = None; - Evd.evar_extra = extra } + Evd.evar_candidates = None } in - let evi = Typeclasses.mark_unresolvable evi in - let (evars, evk) = Evarutil.new_pure_evar_full evars evi in + let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi in let evars = Evd.restore_future_goals evars prev_future_goals in let ctxt = Environ.named_context_of_val hyps in let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in diff --git a/proofs/goal.mli b/proofs/goal.mli index a033d6daab..3b31cff8d7 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -39,16 +39,12 @@ module V82 : sig (* Access to ".evar_concl" *) val concl : Evd.evar_map -> goal -> EConstr.constr - (* Access to ".evar_extra" *) - val extra : Evd.evar_map -> goal -> Evd.Store.t - - (* Old style mk_goal primitive, returns a new goal with corresponding + (* Old style mk_goal primitive, returns a new goal with corresponding hypotheses and conclusion, together with a term which is precisely the evar corresponding to the goal, and an updated evar_map. *) val mk_goal : Evd.evar_map -> Environ.named_context_val -> EConstr.constr -> - Evd.Store.t -> goal * EConstr.constr * Evd.evar_map (* Instantiates a goal with an open term *) diff --git a/proofs/logic.ml b/proofs/logic.ml index 285240872e..254c93d0a2 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -350,7 +350,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let env = Goal.V82.env sigma goal in let hyps = Goal.V82.hyps sigma goal in let mk_goal hyps concl = - Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) + Goal.V82.mk_goal sigma hyps concl in if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in @@ -433,7 +433,7 @@ and mk_hdgoals sigma goal goalacc trm = let env = Goal.V82.env sigma goal in let hyps = Goal.V82.hyps sigma goal in let mk_goal hyps concl = - Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in + Goal.V82.mk_goal sigma hyps concl in match kind trm with | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; diff --git a/proofs/proof.ml b/proofs/proof.ml index 70a08e4966..8220949856 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -386,7 +386,7 @@ let run_tactic env tac pr = (* Check that retrieved given up is empty *) if not (List.is_empty retrieved_given_up) then CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up."); - let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in + let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in Proofview.Unsafe.tclEVARS sigma >>= fun () -> Proofview.tclUNIT retrieved in diff --git a/proofs/refine.ml b/proofs/refine.ml index 05474d5f84..540a8bb420 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -105,7 +105,7 @@ let generic_refine ~typecheck f gl = | Some id -> Evd.rename evk id sigma in (** Mark goals *) - let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in + let sigma = Proofview.Unsafe.mark_as_goals sigma comb in let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Termops.Internal.print_constr_env env sigma c)) in diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 8e296de617..76cbdee0d5 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -226,7 +226,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,ty) in let eqclause = if metas then eqclause - else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd) + else fst (clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)) in let (equiv, args) = EConstr.decompose_app sigma (Clenv.clenv_type eqclause) in let rec split_last_two = function diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 9bd406e14d..81cf9289d1 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -494,15 +494,15 @@ let top_sort evm undefs = let tosee = ref undefs in let rec visit ev evi = let evs = Evarutil.undefined_evars_of_evar_info evm evi in - tosee := Evar.Map.remove ev !tosee; + tosee := Evar.Set.remove ev !tosee; Evar.Set.iter (fun ev -> - if Evar.Map.mem ev !tosee then - visit ev (Evar.Map.find ev !tosee)) evs; + if Evar.Set.mem ev !tosee then + visit ev (Evd.find evm ev)) evs; l' := ev :: !l'; in - while not (Evar.Map.is_empty !tosee) do - let ev, evi = Evar.Map.min_binding !tosee in - visit ev evi + while not (Evar.Set.is_empty !tosee) do + let ev = Evar.Set.choose !tosee in + visit ev (Evd.find evm ev) done; List.rev !l' @@ -512,15 +512,9 @@ let top_sort evm undefs = *) let evars_to_goals p evm = - let goals = ref Evar.Map.empty in - let map ev evi = - let evi, goal = p evm ev evi in - let () = if goal then goals := Evar.Map.add ev evi !goals in - evi - in - let evm = Evd.raw_map_undefined map evm in - if Evar.Map.is_empty !goals then None - else Some (!goals, evm) + let goals, nongoals = Evar.Set.partition (p evm) (Evd.get_typeclass_evars evm) in + if Evar.Set.is_empty goals then None + else Some (goals, nongoals) (** Making local hints *) let make_resolve_hyp env sigma st flags only_classes pri decl = @@ -641,14 +635,6 @@ module Search = struct occur_existential evd concl else true - let mark_unresolvables sigma goals = - List.fold_left - (fun sigma gl -> - let evi = Evd.find_undefined sigma gl in - let evi' = Typeclasses.mark_unresolvable evi in - Evd.add sigma gl evi') - sigma goals - (** The general hint application tactic. tac1 + tac2 .... The choice of OR or ORELSE is determined depending on the dependencies of the goal and the unique/Prop @@ -779,7 +765,7 @@ module Search = struct shelve_goals shelved <*> (if List.is_empty goals then tclUNIT () else - let sigma' = mark_unresolvables sigma goals in + let sigma' = make_unresolvables (fun x -> List.mem_f Evar.equal x goals) sigma in with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state goals)) >>= fun s -> result s i (Some (Option.default 0 k + j))) end @@ -941,14 +927,15 @@ module Search = struct let run_on_evars env evm p tac = match evars_to_goals p evm with | None -> None (* This happens only because there's no evar having p *) - | Some (goals, evm') -> + | Some (goals, nongoals) -> let goals = if !typeclasses_dependency_order then - top_sort evm' goals - else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals) + top_sort evm goals + else Evar.Set.elements goals in + let evm = Evd.set_typeclass_evars evm Evar.Set.empty in let fgoals = Evd.save_future_goals evm in - let _, pv = Proofview.init evm' [] in + let _, pv = Proofview.init evm [] in let pv = Proofview.unshelve goals pv in try let (), pv', (unsafe, shelved, gaveup), _ = @@ -967,7 +954,13 @@ module Search = struct acc && okev) evm' true); let fgoals = Evd.shelve_on_future_goals shelved fgoals in let evm' = Evd.restore_future_goals evm' fgoals in + let nongoals' = + Evar.Set.fold (fun ev acc -> match Evarutil.advance evm' ev with + | Some ev' -> Evar.Set.add ev acc + | None -> acc) nongoals (Evd.get_typeclass_evars evm') + in let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in + let evm' = Evd.set_typeclass_evars evm' nongoals' in Some evm' else raise Not_found with Logic_monad.TacticFailure _ -> raise Not_found @@ -1019,7 +1012,7 @@ let deps_of_constraints cstrs evm p = let evar_dependencies pred evm p = Evd.fold_undefined (fun ev evi _ -> - if Typeclasses.is_resolvable evi && pred evm ev evi then + if Evd.is_typeclass_evar evm ev && pred evm ev evi then let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi) in Intpart.union_set evars p else ()) @@ -1035,8 +1028,7 @@ let split_evars pred evm = let is_inference_forced p evd ev = try - let evi = Evd.find_undefined evd ev in - if Typeclasses.is_resolvable evi && snd (p ev evi) + if Evar.Set.mem ev (Evd.get_typeclass_evars evd) && p ev then let (loc, k) = evar_source ev evd in match k with @@ -1068,55 +1060,32 @@ let error_unresolvable env comp evd = Pretype_errors.unsatisfiable_constraints env evd ev comp (** Check if an evar is concerned by the current resolution attempt, - (and in particular is in the current component), and also update - its evar_info. - Invariant : this should only be applied to undefined evars, - and return undefined evar_info *) + (and in particular is in the current component). + Invariant : this should only be applied to undefined evars. *) -let select_and_update_evars p oevd in_comp evd ev evi = - assert (evi.evar_body == Evar_empty); +let select_and_update_evars p oevd in_comp evd ev = try - let oevi = Evd.find_undefined oevd ev in - if Typeclasses.is_resolvable oevi then - Typeclasses.mark_unresolvable evi, - (in_comp ev && p evd ev evi) - else evi, false - with Not_found -> - Typeclasses.mark_unresolvable evi, p evd ev evi + if Evd.is_typeclass_evar oevd ev then + (in_comp ev && p evd ev (Evd.find evd ev)) + else false + with Not_found -> false (** Do we still have unresolved evars that should be resolved ? *) let has_undefined p oevd evd = - let check ev evi = snd (p oevd ev evi) in + let check ev evi = p oevd ev in Evar.Map.exists check (Evd.undefined_map evd) -(** Revert the resolvability status of evars after resolution, - potentially unprotecting some evars that were set unresolvable - just for this call to resolution. *) - -let revert_resolvability oevd evd = - let map ev evi = - try - if not (Typeclasses.is_resolvable evi) then - let evi' = Evd.find_undefined oevd ev in - if Typeclasses.is_resolvable evi' then - Typeclasses.mark_resolvable evi - else evi - else evi - with Not_found -> evi - in - Evd.raw_map_undefined map evd - exception Unresolved (** If [do_split] is [true], we try to separate the problem in several components and then solve them separately *) let resolve_all_evars debug depth unique env p oevd do_split fail = - let split = if do_split then split_evars p oevd else [Evar.Set.empty] in - let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true - in + let tcs = Evd.get_typeclass_evars oevd in + let split = if do_split then split_evars p oevd else [tcs] in + let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true in let rec docomp evd = function - | [] -> revert_resolvability oevd evd + | [] -> evd | comp :: comps -> let p = select_and_update_evars p oevd (in_comp comp) in try @@ -1134,7 +1103,9 @@ let resolve_all_evars debug depth unique env p oevd do_split fail = let initial_select_evars filter = fun evd ev evi -> - filter ev (snd evi.Evd.evar_source) && + filter ev (Lazy.from_val (snd evi.Evd.evar_source)) && + (** Typeclass evars can contain evars whose conclusion is not + yet determined to be a class or not. *) Typeclasses.is_class_evar evd evi let resolve_typeclass_evars debug depth unique env evd filter split fail = @@ -1161,8 +1132,7 @@ let _ = let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique = let (term, sigma) = Hints.wrap_hint_warning_fun env sigma begin fun sigma -> let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env sigma gl in - let (gl,t,sigma) = - Goal.V82.mk_goal sigma nc gl Store.empty in + let (gl,t,sigma) = Goal.V82.mk_goal sigma nc gl in let (ev, _) = destEvar sigma t in let gls = { it = gl ; sigma = sigma; } in let hints = searchtable_map typeclasses_db in @@ -1227,5 +1197,6 @@ let autoapply c i = unify_e_resolve false flags gl ((c,cty,Univ.ContextSet.empty),0,ce) <*> Proofview.tclEVARMAP >>= (fun sigma -> - let sigma = Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals sigma in + let sigma = Typeclasses.make_unresolvables + (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in Proofview.Unsafe.tclEVARS sigma) end diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index f2bc679aac..6388aa2c33 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -72,11 +72,10 @@ let choose_noteq eqonleft = let generalize_right mk typ c1 c2 = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let store = Proofview.Goal.extra gl in Refine.refine ~typecheck:false begin fun sigma -> let na = Name (next_name_away_with_default "x" Anonymous (Termops.vars_of_env env)) in let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in - let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in + let (sigma, x) = Evarutil.new_evar env sigma ~principal:true newconcl in (sigma, mkApp (x, [|c2|])) end end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 18ddc9318d..a6a104ccca 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -117,14 +117,14 @@ let _ = (** This tactic creates a partial proof realizing the introduction rule, but does not check anything. *) -let unsafe_intro env store decl b = +let unsafe_intro env decl b = Refine.refine ~typecheck:false begin fun sigma -> let ctx = named_context_val env in let nctx = push_named_context_val decl ctx in let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in let ninst = mkRel 1 :: inst in let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in - let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in + let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ninst in (sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) ev) end @@ -133,7 +133,6 @@ let introduction id = let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let hyps = named_context_val (Proofview.Goal.env gl) in - let store = Proofview.Goal.extra gl in let env = Proofview.Goal.env gl in let () = if mem_named_context_val id hyps then user_err ~hdr:"Tactics.introduction" @@ -141,8 +140,8 @@ let introduction id = in let open Context.Named.Declaration in match EConstr.kind sigma concl with - | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b - | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b + | Prod (_, t, b) -> unsafe_intro env (LocalAssum (id, t)) b + | LetIn (_, c, t, b) -> unsafe_intro env (LocalDef (id, c, t)) b | _ -> raise (RefinerError (env, sigma, IntroNeedsProduct)) end @@ -152,7 +151,6 @@ let error msg = CErrors.user_err Pp.(str msg) let convert_concl ?(check=true) ty k = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let store = Proofview.Goal.extra gl in let conclty = Proofview.Goal.concl gl in Refine.refine ~typecheck:false begin fun sigma -> let sigma = @@ -162,7 +160,7 @@ let convert_concl ?(check=true) ty k = | None -> error "Not convertible." | Some sigma -> sigma end else sigma in - let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in + let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ty in let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in (sigma, ans) end @@ -173,11 +171,10 @@ let convert_hyp ?(check=true) d = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ty = Proofview.Goal.concl gl in - let store = Proofview.Goal.extra gl in let sign = convert_hyp check (named_context_val env) sigma d in let env = reset_with_named_context sign env in Refine.refine ~typecheck:false begin fun sigma -> - Evarutil.new_evar env sigma ~principal:true ~store ty + Evarutil.new_evar env sigma ~principal:true ty end end @@ -284,12 +281,11 @@ let move_hyp id dest = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ty = Proofview.Goal.concl gl in - let store = Proofview.Goal.extra gl in let sign = named_context_val env in let sign' = move_hyp_in_named_context env sigma id dest sign in let env = reset_with_named_context sign' env in Refine.refine ~typecheck:false begin fun sigma -> - Evarutil.new_evar env sigma ~principal:true ~store ty + Evarutil.new_evar env sigma ~principal:true ty end end @@ -313,7 +309,6 @@ let rename_hyp repl = Proofview.Goal.enter begin fun gl -> let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in - let store = Proofview.Goal.extra gl in let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in (** Check that we do not mess variables *) @@ -344,7 +339,7 @@ let rename_hyp repl = let nctx = val_of_named_context nhyps in let instance = List.map (NamedDecl.get_id %> mkVar) hyps in Refine.refine ~typecheck:false begin fun sigma -> - Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance + Evarutil.new_evar_instance nctx sigma nconcl ~principal:true instance end end @@ -445,7 +440,6 @@ let internal_cut_gen ?(check=true) dir replace id t = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in - let store = Proofview.Goal.extra gl in let sign = named_context_val env in let sign',t,concl,sigma = if replace then @@ -464,10 +458,10 @@ let internal_cut_gen ?(check=true) dir replace id t = let (sigma,ev,ev') = if dir then let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in - let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in + let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in (sigma,ev,ev') else - let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in + let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in (sigma,ev,ev') in let term = mkLetIn (Name id, ev, t, EConstr.Vars.subst_var id ev') in @@ -2102,11 +2096,10 @@ let keep hyps = let apply_type ~typecheck newcl args = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let store = Proofview.Goal.extra gl in Refine.refine ~typecheck begin fun sigma -> let newcl = nf_betaiota env sigma newcl (* As in former Logic.refine *) in let (sigma, ev) = - Evarutil.new_evar env sigma ~principal:true ~store newcl in + Evarutil.new_evar env sigma ~principal:true newcl in (sigma, applist (ev, args)) end end @@ -2120,13 +2113,12 @@ let bring_hyps hyps = else Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let store = Proofview.Goal.extra gl in let concl = Tacmach.New.pf_concl gl in let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in let args = Array.of_list (Context.Named.to_instance mkVar hyps) in Refine.refine ~typecheck:false begin fun sigma -> let (sigma, ev) = - Evarutil.new_evar env sigma ~principal:true ~store newcl in + Evarutil.new_evar env sigma ~principal:true newcl in (sigma, mkApp (ev, args)) end end @@ -2668,7 +2660,7 @@ let mk_eq_name env id {CAst.loc;v=ido} = (* unsafe *) -let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = +let mkletin_goal env sigma with_eq dep (id,lastlhyp,ccl,c) ty = let open Context.Named.Declaration in let t = match ty with Some t -> t | _ -> typ_of env sigma c in let decl = if dep then LocalDef (id,c,t) @@ -2683,11 +2675,11 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in - let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in + let (sigma, x) = new_evar newenv sigma ~principal:true ccl in (sigma, mkNamedLetIn id c t (mkNamedLetIn heq refl eq x)) | None -> let newenv = insert_before [decl] lastlhyp env in - let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in + let (sigma, x) = new_evar newenv sigma ~principal:true ccl in (sigma, mkNamedLetIn id c t x) let pose_tac na c = @@ -4431,7 +4423,6 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let ccl = Proofview.Goal.concl gl in - let store = Proofview.Goal.extra gl in let check = check_enough_applied env sigma elim in let (sigma', c) = use_bindings env sigma elim false (c0,lbind) t0 in let abs = AbstractPattern (from_prefix,check,Name id,(pending,c),cls,false) in @@ -4457,7 +4448,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim let b = not with_evars && with_eq != None in let (sigma, c) = use_bindings env sigma elim b (c0,lbind) t0 in let t = Retyping.get_type_of env sigma c in - mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t) + mkletin_goal env sigma with_eq false (id,lastlhyp,ccl,c) (Some t) end; if with_evars then Proofview.shelve_unifiable else guard_no_unifiable; if is_arg_pure_hyp @@ -4478,7 +4469,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim let tac = Tacticals.New.tclTHENLIST [ Refine.refine ~typecheck:false begin fun sigma -> - mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None + mkletin_goal env sigma with_eq true (id,lastlhyp,ccl,c) None end; (tac inhyps) ] diff --git a/test-suite/coq-makefile/arg/_CoqProject b/test-suite/coq-makefile/arg/_CoqProject index 53dc963997..ed31a58247 100644 --- a/test-suite/coq-makefile/arg/_CoqProject +++ b/test-suite/coq-makefile/arg/_CoqProject @@ -4,7 +4,7 @@ -arg "-w default" src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/compat-subdirs/_CoqProject b/test-suite/coq-makefile/compat-subdirs/_CoqProject index 4f44bde22a..1f914a71b0 100644 --- a/test-suite/coq-makefile/compat-subdirs/_CoqProject +++ b/test-suite/coq-makefile/compat-subdirs/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/coqdoc1/_CoqProject b/test-suite/coq-makefile/coqdoc1/_CoqProject index 35792066bb..aa9473eaf0 100644 --- a/test-suite/coq-makefile/coqdoc1/_CoqProject +++ b/test-suite/coq-makefile/coqdoc1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/coqdoc2/_CoqProject b/test-suite/coq-makefile/coqdoc2/_CoqProject index d2a547d47b..0068554d72 100644 --- a/test-suite/coq-makefile/coqdoc2/_CoqProject +++ b/test-suite/coq-makefile/coqdoc2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject b/test-suite/coq-makefile/emptyprefix/_CoqProject index 5678a8edbb..3133342f6c 100644 --- a/test-suite/coq-makefile/emptyprefix/_CoqProject +++ b/test-suite/coq-makefile/emptyprefix/_CoqProject @@ -4,7 +4,7 @@ -arg "-w default" src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/extend-subdirs/_CoqProject b/test-suite/coq-makefile/extend-subdirs/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/extend-subdirs/_CoqProject +++ b/test-suite/coq-makefile/extend-subdirs/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/findlib-package/_CoqProject b/test-suite/coq-makefile/findlib-package/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/findlib-package/_CoqProject +++ b/test-suite/coq-makefile/findlib-package/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/latex1/_CoqProject b/test-suite/coq-makefile/latex1/_CoqProject index 35792066bb..aa9473eaf0 100644 --- a/test-suite/coq-makefile/latex1/_CoqProject +++ b/test-suite/coq-makefile/latex1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/merlin1/_CoqProject b/test-suite/coq-makefile/merlin1/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/merlin1/_CoqProject +++ b/test-suite/coq-makefile/merlin1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/mlpack1/_CoqProject b/test-suite/coq-makefile/mlpack1/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/mlpack1/_CoqProject +++ b/test-suite/coq-makefile/mlpack1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/mlpack2/_CoqProject b/test-suite/coq-makefile/mlpack2/_CoqProject index 51864a87ae..3db54e0a0b 100644 --- a/test-suite/coq-makefile/mlpack2/_CoqProject +++ b/test-suite/coq-makefile/mlpack2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/multiroot/_CoqProject b/test-suite/coq-makefile/multiroot/_CoqProject index b384bb6d97..f53eef99a8 100644 --- a/test-suite/coq-makefile/multiroot/_CoqProject +++ b/test-suite/coq-makefile/multiroot/_CoqProject @@ -4,7 +4,7 @@ -I src/ ./src/test_plugin.mllib -./src/test.ml4 +./src/test.mlg ./src/test.mli ./src/test_aux.ml ./src/test_aux.mli diff --git a/test-suite/coq-makefile/native1/_CoqProject b/test-suite/coq-makefile/native1/_CoqProject index a6fa17348c..847b2c00a9 100644 --- a/test-suite/coq-makefile/native1/_CoqProject +++ b/test-suite/coq-makefile/native1/_CoqProject @@ -4,7 +4,7 @@ -arg -native-compiler src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/only/_CoqProject b/test-suite/coq-makefile/only/_CoqProject index 357384fddf..619a8fa459 100644 --- a/test-suite/coq-makefile/only/_CoqProject +++ b/test-suite/coq-makefile/only/_CoqProject @@ -3,7 +3,7 @@ -I src/ ./src/test_plugin.mlpack -./src/test.ml4 +./src/test.mlg ./src/test.mli ./src/test_aux.ml ./src/test_aux.mli diff --git a/test-suite/coq-makefile/plugin1/_CoqProject b/test-suite/coq-makefile/plugin1/_CoqProject index 4eddc9d708..ab7876d868 100644 --- a/test-suite/coq-makefile/plugin1/_CoqProject +++ b/test-suite/coq-makefile/plugin1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mllib -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/plugin2/_CoqProject b/test-suite/coq-makefile/plugin2/_CoqProject index 0bf1e07f25..94eed53130 100644 --- a/test-suite/coq-makefile/plugin2/_CoqProject +++ b/test-suite/coq-makefile/plugin2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mllib -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/plugin3/_CoqProject b/test-suite/coq-makefile/plugin3/_CoqProject index 2028d49a8b..8e8a7ab074 100644 --- a/test-suite/coq-makefile/plugin3/_CoqProject +++ b/test-suite/coq-makefile/plugin3/_CoqProject @@ -3,7 +3,7 @@ -I src/ ./src/test_plugin.mllib -./src/test.ml4 +./src/test.mlg ./src/test.mli ./src/test_aux.ml ./src/test_aux.mli diff --git a/test-suite/coq-makefile/quick2vo/_CoqProject b/test-suite/coq-makefile/quick2vo/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/quick2vo/_CoqProject +++ b/test-suite/coq-makefile/quick2vo/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index 2e066d30d9..30be5e6456 100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -11,7 +11,7 @@ mkdir -p theories/sub cp ../../template/theories/sub/testsub.v theories/sub cp ../../template/theories/test.v theories -cp ../../template/src/test.ml4 src +cp ../../template/src/test.mlg src cp ../../template/src/test_aux.mli src cp ../../template/src/test.mli src cp ../../template/src/test_plugin.mlpack src diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.mlg index 72765abe04..7a166f3b98 100644 --- a/test-suite/coq-makefile/template/src/test.ml4 +++ b/test-suite/coq-makefile/template/src/test.mlg @@ -1,13 +1,17 @@ +{ open Ltac_plugin +} DECLARE PLUGIN "test_plugin" +{ let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; +} VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF - | [ "TestCommand" ] -> [ () ] + | [ "TestCommand" ] -> { () } END TACTIC EXTEND test -| [ "test_tactic" ] -> [ Test_aux.tac ] +| [ "test_tactic" ] -> { Test_aux.tac } END diff --git a/test-suite/coq-makefile/uninstall1/_CoqProject b/test-suite/coq-makefile/uninstall1/_CoqProject index 35792066bb..aa9473eaf0 100644 --- a/test-suite/coq-makefile/uninstall1/_CoqProject +++ b/test-suite/coq-makefile/uninstall1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/uninstall2/_CoqProject b/test-suite/coq-makefile/uninstall2/_CoqProject index d2a547d47b..0068554d72 100644 --- a/test-suite/coq-makefile/uninstall2/_CoqProject +++ b/test-suite/coq-makefile/uninstall2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/validate1/_CoqProject b/test-suite/coq-makefile/validate1/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/validate1/_CoqProject +++ b/test-suite/coq-makefile/validate1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/vio2vo/_CoqProject b/test-suite/coq-makefile/vio2vo/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/vio2vo/_CoqProject +++ b/test-suite/coq-makefile/vio2vo/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/misc/poly-capture-global-univs/_CoqProject b/test-suite/misc/poly-capture-global-univs/_CoqProject index 70ec246062..e5dc3cff56 100644 --- a/test-suite/misc/poly-capture-global-univs/_CoqProject +++ b/test-suite/misc/poly-capture-global-univs/_CoqProject @@ -1,7 +1,7 @@ -Q theories Evil -I src -src/evil.ml4 +src/evil.mlg src/evilImpl.ml src/evilImpl.mli src/evil_plugin.mlpack diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.ml4 b/test-suite/misc/poly-capture-global-univs/src/evil.ml4 deleted file mode 100644 index 565e979aaa..0000000000 --- a/test-suite/misc/poly-capture-global-univs/src/evil.ml4 +++ /dev/null @@ -1,9 +0,0 @@ - -open Stdarg -open EvilImpl - -DECLARE PLUGIN "evil_plugin" - -VERNAC COMMAND FUNCTIONAL EXTEND VernacEvil CLASSIFIED AS SIDEFF -| [ "Evil" ident(x) ident(y) ] -> [ fun ~atts ~st -> evil x y; st ] -END diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.mlg b/test-suite/misc/poly-capture-global-univs/src/evil.mlg new file mode 100644 index 0000000000..edd22b1d29 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evil.mlg @@ -0,0 +1,10 @@ +{ +open Stdarg +open EvilImpl +} + +DECLARE PLUGIN "evil_plugin" + +VERNAC COMMAND EXTEND VernacEvil CLASSIFIED AS SIDEFF +| [ "Evil" ident(x) ident(y) ] -> { evil x y } +END diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 403ad61798..e3fa0c24fe 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -21,6 +21,7 @@ VFILES := $(COQMF_VFILES) MLIFILES := $(COQMF_MLIFILES) MLFILES := $(COQMF_MLFILES) ML4FILES := $(COQMF_ML4FILES) +MLGFILES := $(COQMF_MLGFILES) MLPACKFILES := $(COQMF_MLPACKFILES) MLLIBFILES := $(COQMF_MLLIBFILES) CMDLINE_VFILES := $(COQMF_CMDLINE_VFILES) @@ -87,6 +88,7 @@ COQTOP ?= "$(COQBIN)coqtop" COQCHK ?= "$(COQBIN)coqchk" COQDEP ?= "$(COQBIN)coqdep" COQDOC ?= "$(COQBIN)coqdoc" +COQPP ?= "$(COQBIN)coqpp" COQMKFILE ?= "$(COQBIN)coq_makefile" # Timing scripts @@ -241,6 +243,7 @@ VDFILE := .coqdeps ALLSRCFILES := \ $(ML4FILES) \ + $(MLGFILES) \ $(MLFILES) \ $(MLPACKFILES) \ $(MLLIBFILES) \ @@ -262,6 +265,7 @@ TEXFILES = $(VFILES:.v=.tex) GTEXFILES = $(VFILES:.v=.g.tex) CMOFILES = \ $(ML4FILES:.ml4=.cmo) \ + $(MLGFILES:.mlg=.cmo) \ $(MLFILES:.ml=.cmo) \ $(MLPACKFILES:.mlpack=.cmo) CMXFILES = $(CMOFILES:.cmo=.cmx) @@ -277,7 +281,7 @@ CMXSFILES = \ $(MLPACKFILES:.mlpack=.cmxs) \ $(CMXAFILES:.cmxa=.cmxs) \ $(if $(MLPACKFILES)$(CMXAFILES),,\ - $(ML4FILES:.ml4=.cmxs) $(MLFILES:.ml=.cmxs)) + $(ML4FILES:.ml4=.cmxs) $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs)) # files that are packed into a plugin (no extension) PACKEDFILES = \ @@ -555,6 +559,7 @@ clean:: $(HIDE)rm -f $(CMXSFILES) $(HIDE)rm -f $(CMOFILES:.cmo=.o) $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) + $(HIDE)rm -f $(MLGFILES:.mlg=.ml) $(HIDE)rm -f $(ALLDFILES) $(HIDE)rm -f $(NATIVEFILES) $(HIDE)find . -name .coq-native -type d -empty -delete @@ -602,11 +607,17 @@ $(ML4FILES:.ml4=.cmx): %.cmx: %.ml4 $(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<' $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $< -$(MLFILES:.ml=.cmo): %.cmo: %.ml +$(MLGFILES:.mlg=.ml): %.ml: %.mlg + $(SHOW)'COQPP $<' + $(HIDE)$(COQPP) $< + +# Stupid hack around a deficient syntax: we cannot concatenate two expansions +$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml $(SHOW)'CAMLC -c $<' $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< -$(MLFILES:.ml=.cmx): %.cmx: %.ml +# Same hack +$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< @@ -647,7 +658,7 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ # This rule is for _CoqProject with no .mllib nor .mlpack -$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx +$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ -shared -o $@ $< @@ -716,6 +727,10 @@ $(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4 $(SHOW)'CAMLDEP -pp $<' $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok) +$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + $(addsuffix .d,$(MLFILES)): %.ml.d: %.ml $(SHOW)'CAMLDEP $<' $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 7bb1390cad..ca5a232edb 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -218,7 +218,7 @@ let generate_conf_coq_config oc = ;; let generate_conf_files oc - { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files; } + { v_files; mli_files; ml4_files; mlg_files; ml_files; mllib_files; mlpack_files; } = let module S = String in let map = map_sourced_list in @@ -227,6 +227,7 @@ let generate_conf_files oc fprintf oc "COQMF_MLIFILES = %s\n" (S.concat " " (map quote mli_files)); fprintf oc "COQMF_MLFILES = %s\n" (S.concat " " (map quote ml_files)); fprintf oc "COQMF_ML4FILES = %s\n" (S.concat " " (map quote ml4_files)); + fprintf oc "COQMF_MLGFILES = %s\n" (S.concat " " (map quote mlg_files)); fprintf oc "COQMF_MLPACKFILES = %s\n" (S.concat " " (map quote mlpack_files)); fprintf oc "COQMF_MLLIBFILES = %s\n" (S.concat " " (map quote mllib_files)); let cmdline_vfiles = filter_cmdline v_files in @@ -283,7 +284,7 @@ let generate_conf oc project args = let ensure_root_dir ({ ml_includes; r_includes; q_includes; - v_files; ml_files; mli_files; ml4_files; + v_files; ml_files; mli_files; ml4_files; mlg_files; mllib_files; mlpack_files } as project) = let exists f = List.exists (forget_source > f) in @@ -293,8 +294,8 @@ let ensure_root_dir || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes || (not_tops v_files && - not_tops mli_files && not_tops ml4_files && not_tops ml_files && - not_tops mllib_files && not_tops mlpack_files) + not_tops mli_files && not_tops ml4_files && not_tops mlg_files && + not_tops ml_files && not_tops mllib_files && not_tops mlpack_files) then project else diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 6a913ea894..713b2ad2b6 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -496,9 +496,9 @@ let rec suffixes = function let add_caml_known phys_dir _ f = let basename,suff = - get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] in + get_extension f [".ml";".mli";".ml4";".mlg";".mllib";".mlpack"] in match suff with - | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff + | ".ml"|".ml4"|".mlg" -> add_ml_known basename (Some phys_dir) suff | ".mli" -> add_mli_known basename (Some phys_dir) suff | ".mllib" -> add_mllib_known basename (Some phys_dir) suff | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff @@ -584,12 +584,12 @@ let rec treat_file old_dirname old_name = in Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name)) | S_REG -> - (match get_extension name [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with + (match get_extension name [".v";".ml";".mli";".ml4";".mlg";".mllib";".mlpack"] with | (base,".v") -> let name = file_name base dirname and absname = absolute_file_name base dirname in addQueue vAccu (name, absname) - | (base,(".ml"|".ml4" as ext)) -> addQueue mlAccu (base,ext,dirname) + | (base,(".ml"|".ml4"|".mlg" as ext)) -> addQueue mlAccu (base,ext,dirname) | (base,".mli") -> addQueue mliAccu (base,dirname) | (base,".mllib") -> addQueue mllibAccu (base,dirname) | (base,".mlpack") -> addQueue mlpackAccu (base,dirname) diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index 053a0435ce..155296362f 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -145,9 +145,9 @@ let mllibAccu = ref ([] : (string * dir) list) let mlpackAccu = ref ([] : (string * dir) list) let add_caml_known phys_dir f = - let basename,suff = get_extension f [".ml";".ml4";".mlpack"] in + let basename,suff = get_extension f [".ml";".ml4";".mlg";".mlpack"] in match suff with - | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff + | ".ml"|".ml4"|".mlg" -> add_ml_known basename (Some phys_dir) suff | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff | _ -> () diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 885a22b209..5ff3032ec4 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -102,10 +102,6 @@ let mk_mltype_data sigma env assums arity indname = let is_ml_type = is_sort env sigma arity in (is_ml_type,indname,assums) -let prepare_param = function - | LocalAssum (na,t) -> Name.get_id na, LocalAssumEntry t - | LocalDef (na,b,_) -> Name.get_id na, LocalDefEntry b - (** Make the arity conclusion flexible to avoid generating an upper bound universe now, only if the universe does not appear anywhere else. This is really a hack to stay compatible with the semantics of template polymorphic @@ -463,7 +459,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not in (* Build the mutual inductive entry *) let mind_ent = - { mind_entry_params = List.map prepare_param ctx_params; + { mind_entry_params = ctx_params; mind_entry_record = None; mind_entry_finite = finite; mind_entry_inds = entries; diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a4b3a75c9f..ca77e03707 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -773,12 +773,13 @@ let pr_constraints printenv env sigma evars cstrs = let explain_unsatisfiable_constraints env sigma constr comp = let (_, constraints) = Evd.extract_all_conv_pbs sigma in + let tcs = Evd.get_typeclass_evars sigma in let undef = Evd.undefined_map sigma in (** Only keep evars that are subject to resolution and members of the given component. *) - let is_kept evk evi = match comp with - | None -> Typeclasses.is_resolvable evi - | Some comp -> Typeclasses.is_resolvable evi && Evar.Set.mem evk comp + let is_kept evk _ = match comp with + | None -> Evar.Set.mem evk tcs + | Some comp -> Evar.Set.mem evk tcs && Evar.Set.mem evk comp in let undef = let m = Evar.Map.filter is_kept undef in diff --git a/vernac/record.ml b/vernac/record.ml index 3ba360fee4..7a4c38e972 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -191,14 +191,6 @@ let typecheck_params_and_fields finite def poly pl ps records = let ans = List.map2 map data typs in ubinders, univs, template, newps, imps, ans -let degenerate_decl decl = - let id = match RelDecl.get_name decl with - | Name id -> id - | Anonymous -> anomaly (Pp.str "Unnamed record variable.") in - match decl with - | LocalAssum (_,t) -> (id, LocalAssumEntry t) - | LocalDef (_,b,_) -> (id, LocalDefEntry b) - type record_error = | MissingProj of Id.t * Id.t list | BadTypedProj of Id.t * env * Type_errors.type_error @@ -437,7 +429,7 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St in let blocks = List.mapi mk_block record_data in let mie = - { mind_entry_params = List.map degenerate_decl params; + { mind_entry_params = params; mind_entry_record = Some (if !primitive_flag then Some binder_name else None); mind_entry_finite = finite; mind_entry_inds = blocks; |