diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 10 | ||||
| -rw-r--r-- | interp/declare.ml | 21 |
2 files changed, 17 insertions, 14 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 = |