From 7dd28b4772251af6ae3641ec63a8251153915e21 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 26 Feb 2013 18:52:05 +0000 Subject: Names: shortcuts for building {kn, constant, mind} with empty sections git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16249 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/mod_subst.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'kernel/mod_subst.ml') diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 6d558bf3c..731475fb4 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -190,16 +190,16 @@ let kn_of_deltas resolve1 resolve2 kn = if kn' == kn then kn_of_delta resolve2 kn else kn' let constant_of_delta_kn resolve kn = - Constant.make2 kn (kn_of_delta resolve kn) + Constant.make kn (kn_of_delta resolve kn) let constant_of_deltas_kn resolve1 resolve2 kn = - Constant.make2 kn (kn_of_deltas resolve1 resolve2 kn) + Constant.make kn (kn_of_deltas resolve1 resolve2 kn) let mind_of_delta_kn resolve kn = - MutInd.make2 kn (kn_of_delta resolve kn) + MutInd.make kn (kn_of_delta resolve kn) let mind_of_deltas_kn resolve1 resolve2 kn = - MutInd.make2 kn (kn_of_deltas resolve1 resolve2 kn) + MutInd.make kn (kn_of_deltas resolve1 resolve2 kn) let inline_of_delta inline resolver = match inline with @@ -288,7 +288,7 @@ let subst_ind sub mind = let knc' = progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc in - MutInd.make2 knu knc' + MutInd.make knu knc' with No_subst -> mind let subst_con0 sub cst = @@ -305,7 +305,7 @@ let subst_con0 sub cst = let knc' = progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc in - let cst' = Constant.make2 knu knc' in + let cst' = Constant.make knu knc' in cst', mkConst cst' let subst_con sub cst = -- cgit v1.2.3