diff options
| -rw-r--r-- | checker/declarations.ml | 10 | ||||
| -rw-r--r-- | checker/declarations.mli | 1 | ||||
| -rw-r--r-- | checker/modops.ml | 4 | ||||
| -rw-r--r-- | checker/term.ml | 2 | ||||
| -rw-r--r-- | checker/validate.ml | 9 |
5 files changed, 15 insertions, 11 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 95d1f2bd1..2a5d3114c 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -64,13 +64,13 @@ let empty_delta_resolver = Deltamap.empty type substitution = (module_path * delta_resolver) Umap.t type 'a subst_fun = substitution -> 'a -> 'a -let val_res_dom = no_val - (*val_sum "resolver_domain" 0 [|[|val_kn|];[|val_mp|]|]*) +let val_res_dom = + val_sum "delta_key" 0 [|[|val_kn|];[|val_mp|]|] -let val_res = no_val - (* val_map ~name:"delta_resolver" +let val_res = + val_map ~name:"delta_resolver" val_res_dom - (val_sum "resolver_codomain" 0 [|[|val_opt val_constr||];[|val_kn|];[|val_mp|]|])*) + (val_sum "delta_hint" 0 [|[|val_opt val_constr|];[|val_kn|];[|val_mp|]|]) let val_subst = val_map ~name:"substitution" diff --git a/checker/declarations.mli b/checker/declarations.mli index bae7da908..8afe09dac 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -198,6 +198,7 @@ val add_mbid : mod_bound_id -> module_path -> substitution -> substitution val add_mp : module_path -> module_path -> substitution -> substitution val map_mbid : mod_bound_id -> module_path -> substitution val map_mp : module_path -> module_path -> substitution +val mp_in_delta : module_path -> delta_resolver -> bool val subst_const_body : constant_body subst_fun val subst_mind : mutual_inductive_body subst_fun diff --git a/checker/modops.ml b/checker/modops.ml index de0d6c7e9..ce2f07ab6 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -127,7 +127,9 @@ let strengthen_const env mp_from l cb resolver = let rec strengthen_mod env mp_from mp_to mb = - assert(mp_from = mb.mod_mp); + if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then + mb + else match mb.mod_type with | SEBstruct (sign) -> let resolve_out,sign_out = diff --git a/checker/term.ml b/checker/term.ml index 658eac4f0..d9ecaaea5 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -116,7 +116,7 @@ let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [| [|val_name;val_constr;val_constr|]; (* Lambda *) [|val_name;val_constr;val_constr;val_constr|]; (* LetIn *) [|val_constr;val_array val_constr|]; (* App *) - [|val_kn|]; (* Const *) + [|val_con|]; (* Const *) [|val_ind|]; (* Ind *) [|val_cstr|]; (* Construct *) [|val_ci;val_constr;val_constr;val_array val_constr|]; (* Case *) diff --git a/checker/validate.ml b/checker/validate.ml index 704468169..ab17aa7f8 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -164,11 +164,12 @@ let val_mp = val_rec_sum "module_path" 0 (fun vmp -> [|[|val_dp|];[|val_uid|];[|vmp;val_id|]|]) -let val_kn = - let val_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|] in - val_tuple "kn*kn" [|val_kn;val_kn|] +let val_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|] -let val_ind = val_tuple "inductive"[|val_kn;val_int|] +let val_con = + val_tuple "constant/mutind" [|val_kn;val_kn|] + +let val_ind = val_tuple "inductive"[|val_con;val_int|] let val_cstr = val_tuple "constructor"[|val_ind;val_int|] (* univ *) |