From 2b09b02c136d3d68fa19e4493d5b5ad28c4f16db Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 26 Feb 2013 18:51:57 +0000 Subject: Names: Modularize constant and mutual_inductive git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16248 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/declarations.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'checker/declarations.ml') diff --git a/checker/declarations.ml b/checker/declarations.ml index 529f08cb1..2ff570a4a 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -223,6 +223,11 @@ let gen_subst_mp f sub mp1 mp2 = | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2 +let make_mind_equiv mpu mpc dir l = + let knu = make_kn mpu dir l in + if mpu == mpc then mind_of_kn knu + else mind_of_kn_equiv knu (make_kn mpc dir l) + let subst_ind sub mind = let kn1,kn2 = user_mind mind, canonical_mind mind in let mp1,dir,l = repr_kn kn1 in @@ -235,6 +240,11 @@ let subst_ind sub mind = | Canonical -> mind_of_delta2 resolve mind' with No_subst -> mind +let make_con_equiv mpu mpc dir l = + let knu = make_kn mpu dir l in + if mpu == mpc then constant_of_kn knu + else constant_of_kn_equiv knu (make_kn mpc dir l) + let subst_con0 sub con = let kn1,kn2 = user_con con,canonical_con con in let mp1,dir,l = repr_kn kn1 in -- cgit v1.2.3