From eece7fc7d2de6e3097703c4276f79aa12eb0e011 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 13 Oct 2002 13:19:48 +0000
Subject: Moins de restriction sur le commit précédent

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

diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
index 0bb144867b..ea50976696 100644
--- a/pretyping/syntax_def.ml
+++ b/pretyping/syntax_def.ml
@@ -71,6 +71,9 @@ let rec set_loc loc = function
   | RApp (_,a,b)    -> RApp (loc,set_loc loc a,List.map (set_loc loc) b)
   | RSort (_,a)      -> RSort (loc,a) 
   | RHole (_,a)      -> RHole (loc,a)
+  | 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)
   | a -> warning "Unrelocatated syntactic definition"; a
 
 let search_syntactic_definition loc kn =
-- 
cgit v1.2.3