diff options
| -rw-r--r-- | kernel/declareops.ml | 2 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 4 | ||||
| -rw-r--r-- | library/declare.ml | 22 | ||||
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_110.v (renamed from test-suite/bugs/opened/HoTT_coq_110.v) | 4 | ||||
| -rw-r--r-- | toplevel/ind_tables.ml | 10 |
5 files changed, 28 insertions, 14 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index dd906bab24..149eeba287 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -284,7 +284,7 @@ type side_effects = side_effect list let no_seff = ([] : side_effects) let iter_side_effects f l = List.iter f (List.rev l) let fold_side_effects f a l = List.fold_left f a l -let uniquize_side_effects l = l (** FIXME: there is something dubious here *) +let uniquize_side_effects l = CList.uniquize l let union_side_effects l1 l2 = l1 @ l2 let flatten_side_effects l = List.flatten l let side_effects_of_list l = l diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 8c4ec8cbfc..770c720d89 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -64,6 +64,10 @@ let handle_side_effects env body side_eff = let cbl = match se with | SEsubproof (c,cb) -> [c,cb] | SEscheme (cl,_) -> List.map (fun (_,c,cb) -> c,cb) cl in + let not_exists (c,_) = + try ignore(Environ.lookup_constant c env); false + with Not_found -> true in + let cbl = List.filter not_exists cbl in let cname c = let name = string_of_con c in for i = 0 to String.length name - 1 do diff --git a/library/declare.ml b/library/declare.ml index 4364461ef5..dce346782c 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -208,11 +208,11 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types let declare_scheme = ref (fun _ _ -> assert false) let set_declare_scheme f = declare_scheme := f -let declare_sideff fix_exn se = +let declare_sideff env fix_exn se = let cbl, scheme = match se with | SEsubproof (c, cb) -> [c, cb], None | SEscheme (cbl, k) -> - List.map (fun (_,c,cb) -> c,cb) cbl, Some (List.map pi1 cbl,k) in + List.map (fun (_,c,cb) -> c,cb) cbl, Some (cbl,k) in let id_of c = Names.Label.to_id (Names.Constant.label c) in let pt_opaque_of cb = match cb with @@ -243,13 +243,21 @@ let declare_sideff fix_exn se = cst_kind = Decl_kinds.IsDefinition Decl_kinds.Definition; cst_locl = true; } in + let exists c = + try ignore(Environ.lookup_constant c env); true + with Not_found -> false in let knl = - List.map (fun (c,cb) -> - declare_constant_common (id_of c) (cst_of cb)) cbl in + CList.map_filter (fun (c,cb) -> + if exists c then None + else Some (c,declare_constant_common (id_of c) (cst_of cb))) cbl in match scheme with | None -> () - | Some (inds,kind) -> - !declare_scheme kind (Array.of_list (List.combine inds knl)) + | Some (inds_consts,kind) -> + !declare_scheme kind (Array.of_list + (List.map (fun (c,kn) -> + CList.find_map (fun (x,c',_) -> + if Constant.equal c c' then Some (x,kn) else None) inds_consts) + knl)) let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) = let cd = (* We deal with side effects of non-opaque constants *) @@ -264,7 +272,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) = else begin let seff = Declareops.uniquize_side_effects seff in Declareops.iter_side_effects - (declare_sideff (Future.fix_exn_of bo)) seff; + (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff; Entries.DefinitionEntry { de with const_entry_body = Future.chain ~pure:true bo (fun (pt, _) -> pt, Declareops.no_seff) } diff --git a/test-suite/bugs/opened/HoTT_coq_110.v b/test-suite/bugs/closed/HoTT_coq_110.v index c9874f898c..5ec40dbcb9 100644 --- a/test-suite/bugs/opened/HoTT_coq_110.v +++ b/test-suite/bugs/closed/HoTT_coq_110.v @@ -19,5 +19,5 @@ Module Y. Definition foo : (A = B) * (A = B). split; abstract (rewrite <- P; reflexivity). (* Error: internal_paths_rew already exists. *) - Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *) -Fail End Y. + Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *) +End Y. diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 1ee2adcd8c..1f09d76205 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -181,12 +181,14 @@ let define_mutual_scheme kind internal names mind = define_mutual_scheme_base kind s f internal names mind let find_scheme_on_env_too kind ind = - String.Map.find kind (Indmap.find ind !scheme_map) + let s = String.Map.find kind (Indmap.find ind !scheme_map) in + s, Declareops.cons_side_effects + (Safe_typing.sideff_of_scheme + kind (Global.safe_env()) [ind, s]) + Declareops.no_seff let find_scheme kind (mind,i as ind) = - try - let s = find_scheme_on_env_too kind ind in - s, Declareops.no_seff + try find_scheme_on_env_too kind ind with Not_found -> match Hashtbl.find scheme_object_table kind with | s,IndividualSchemeFunction f -> |