From ab058ba005b1a6e91a87973006ebac823d7722e3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 14 Sep 2000 07:25:35 +0000
Subject: Abstraction de constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/inductive.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2f5e02ad43..33d15798a4 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -67,7 +67,7 @@ let mis_type_nf_mconstruct i mispec =
   let specif = mis_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
-  let make_Ik k = DOPN(MutInd(mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
+  let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
   if i > nconstr then error "Not enough constructors in the type";
   substl (list_tabulate make_Ik ntypes) specif.(i-1)
 
@@ -75,7 +75,7 @@ let mis_type_mconstruct i mispec =
   let specif = mis_typed_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
-  let make_Ik k = DOPN(MutInd(mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
+  let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
   if i > nconstr then error "Not enough constructors in the type";
   typed_app (substl (list_tabulate make_Ik ntypes)) specif.(i-1)
 
-- 
cgit v1.2.3