diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 8 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 11 | ||||
| -rw-r--r-- | pretyping/recordops.mli | 1 |
3 files changed, 14 insertions, 6 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 862865bd90..037006bc47 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -455,7 +455,9 @@ let rec decomp_branch tags nal flags (avoid,env as e) sigma c = (avoid', add_name_opt na' body t env) sigma c let rec build_tree na isgoal e sigma ci cl = - let mkpat n rhs pl = DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in + let mkpat n rhs pl = + let na = update_name sigma na rhs in + na, DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,na) in let cnl = ci.ci_pp_info.cstr_tags in List.flatten (List.init (Array.length cl) @@ -485,7 +487,9 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with and contract_branch isgoal e sigma (cdn,mkpat,rhs) = let nal,rhs = decomp_branch cdn [] isgoal e sigma rhs in let mat = align_tree nal isgoal rhs sigma in - List.map (fun (ids,hd,rhs) -> ids,mkpat rhs hd,rhs) mat + List.map (fun (ids,hd,rhs) -> + let na, pat = mkpat rhs hd in + (Nameops.Name.fold_right Id.Set.add na ids, pat, rhs)) mat (**********************************************************************) (* Transform internal representation of pattern-matching into list of *) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 5b416a99f9..35e182840b 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -114,7 +114,7 @@ let find_primitive_projection c = (* the effective components of a structure and the projections of the *) (* structure *) -(* Table des definitions "object" : pour chaque object c, +(* Table of "object" definitions: for each object c, c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n) @@ -127,16 +127,19 @@ let find_primitive_projection c = that maps the pair (Li,ci) to the following data + o_ORIGIN = c (the constant name which this conversion rule is + synthesized from) o_DEF = c o_TABS = B1...Bk o_INJ = Some n (when ci is a reference to the parameter xi) - o_PARAMS = a1...am - o_NARAMS = m + o_TPARAMS = a1...am + o_NPARAMS = m o_TCOMP = ui1...uir *) type obj_typ = { + o_ORIGIN : Constant.t; o_DEF : constr; o_CTX : Univ.AUContext.t; o_INJ : int option; (* position of trivial argument if any *) @@ -224,7 +227,7 @@ let compute_canonical_projections env ~warn (con,ind) = match cs_pattern_of_constr nenv t with | patt, o_INJ, o_TCOMPS -> ((GlobRef.ConstRef proji_sp, (patt, t)), - { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) + { o_ORIGIN = con ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) :: acc | exception Not_found -> if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp); diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index e8b0d771aa..aaba7cc3e5 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -73,6 +73,7 @@ type cs_pattern = | Default_cs type obj_typ = { + o_ORIGIN : Constant.t; o_DEF : constr; o_CTX : Univ.AUContext.t; o_INJ : int option; (** position of trivial argument *) |