summaryrefslogtreecommitdiff
path: root/pretyping/rawterm.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /pretyping/rawterm.ml
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'pretyping/rawterm.ml')
-rw-r--r--pretyping/rawterm.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 3726b8df..30b62ea8 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: rawterm.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: rawterm.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
(*i*)
open Util
@@ -219,7 +219,7 @@ let free_rawvars =
| RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) ->
let vs' = vars bounded vs ty in
let bounded' = add_name_to_ids bounded na in
- vars bounded' vs' c
+ vars bounded' vs' c
| RCases (loc,sty,rtntypopt,tml,pl) ->
let vs1 = vars_option bounded vs rtntypopt in
let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in