From 1c795ed9386af88b76c4eb591c751aaa1fab7bfd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 17 Oct 2002 10:59:46 +0000
Subject: Moins de restriction sur le commit 1.5

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

diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
index ea50976696..cb1be3ebb8 100644
--- a/pretyping/syntax_def.ml
+++ b/pretyping/syntax_def.ml
@@ -74,6 +74,7 @@ let rec set_loc loc = function
   | RLambda (_,na,ty,c) -> RLambda (loc,na,set_loc loc ty,set_loc loc c)
   | RProd (_,na,ty,c) -> RProd (loc,na,set_loc loc ty,set_loc loc c)
   | RLetIn (_,na,b,c) -> RLetIn (loc,na,set_loc loc b,set_loc loc c)
+  | RCast (_,a,b) -> RCast (loc,set_loc loc a,set_loc loc b)
   | a -> warning "Unrelocatated syntactic definition"; a
 
 let search_syntactic_definition loc kn =
-- 
cgit v1.2.3