diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 10 | ||||
| -rw-r--r-- | interp/declare.ml | 21 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 2 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.mli | 8 |
4 files changed, 22 insertions, 19 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4e217b2cdd..18d6c1a5b7 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -710,10 +710,12 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let arg = match arg with | None -> None | Some arg -> - let mk_env (c, (tmp_scope, subscopes)) = + let mk_env id (c, (tmp_scope, subscopes)) map = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in - let gc = intern nenv c in - (gc, Some c) + try + let gc = intern nenv c in + Id.Map.add id (gc, Some c) map + with GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in @@ -725,7 +727,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = | [pat] -> (glob_constr_of_cases_pattern pat, None) | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () in - let terms = Id.Map.map mk_env terms in + let terms = Id.Map.fold mk_env terms Id.Map.empty in let binders = Id.Map.map mk_env' binders in let bindings = Id.Map.fold Id.Map.add terms binders in Some (Genintern.generic_substitute_notation bindings arg) diff --git a/interp/declare.ml b/interp/declare.ml index e79cc60798..fcb62ac8c4 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -383,13 +383,12 @@ let inInductive : inductive_obj -> obj = rebuild_function = infer_inductive_subtyping } let declare_projections univs mind = - (** FIXME: handle mutual records *) - let mind = (mind, 0) in let env = Global.env () in - let spec,_ = Inductive.lookup_mind_specif env mind in - match spec.mind_record with - | PrimRecord info -> - let _, kns, _ = info.(0) in + let mib = Environ.lookup_mind mind env in + match mib.mind_record with + | PrimRecord info -> + let iter i (_, kns, _) = + let mind = (mind, i) in let projs = Inductiveops.compute_projections env mind in Array.iter2 (fun kn (term, types) -> let id = Label.to_id (Constant.label kn) in @@ -411,10 +410,12 @@ let declare_projections univs mind = let entry = definition_entry ~types ~univs term in let kn' = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in assert (Constant.equal kn kn') - ) kns projs; - true, true - | FakeRecord -> true,false - | NotRecord -> false,false + ) kns projs + in + let () = Array.iteri iter info in + true, true + | FakeRecord -> true, false + | NotRecord -> false, false (* for initial declaration *) let declare_mind mie = diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 83ad9af338..288a0bfe00 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -22,7 +22,7 @@ open Libobject open Nameops open Context.Rel.Declaration -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *) +exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m)) module RelDecl = Context.Rel.Declaration diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index a8492095ec..437fef1753 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -38,14 +38,14 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits val combine_params_freevar : - Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t -> + Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> Constrexpr.constr_expr * Id.Set.t val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t -> + (Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> Constrexpr.constr_expr * Id.Set.t) -> constr_expr -> constr_expr * Id.Set.t (* Should be likely located elsewhere *) -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *) -val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Context.Rel.t -> 'a +exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) +val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Constr.rel_context -> 'a |