diff options
| author | herbelin | 2002-10-17 10:59:46 +0000 |
|---|---|---|
| committer | herbelin | 2002-10-17 10:59:46 +0000 |
| commit | 1c795ed9386af88b76c4eb591c751aaa1fab7bfd (patch) | |
| tree | e3b09d798625b69f5276e0d744b75909d348390d | |
| parent | 27958fd8bf2ed0f2811011f0854d6d0af4ae4834 (diff) | |
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
| -rw-r--r-- | pretyping/syntax_def.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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 = |