From 15da5979d322c5da5f251dfd92da26407df5e45f Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 9 Oct 2002 15:42:49 +0000
Subject: retour en arriere concernant la recherche d'occurence modulo
 expansion des letins, ce qui conduisait a des comportement peu intuitifs. On
 priviligiera l'utilisation de la tactique Subst.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3110 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/record.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/record.ml b/toplevel/record.ml
index 9edb4e1d54..60855b2fc7 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -205,7 +205,6 @@ let definition_structure ((is_coe,idstruc),ps,cfs,idbuild,s) =
   let extract_name = function Vernacexpr.AssumExpr(id,_) -> id | Vernacexpr.DefExpr (id,_,_) -> id in
   let allnames =  idstruc::idps@(List.map extract_name fs) in
   if not (list_distinct allnames) then error "Two objects have the same name";
-  if occur_fields idstruc fs then error "A record cannot be recursive";
   (* Now, younger decl in params and fields is on top *)
   let params,fields = typecheck_params_and_fields ps fs in
 (*  let args =  List.map mkVar idps in*)
-- 
cgit v1.2.3