From 67787e6daeb7bf2fe59d5546969197ca9f87c2dc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 29 Mar 2003 14:06:47 +0000
Subject: Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3806 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/correctness/pcic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib')

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index e3852504a6..66ac7b97e9 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -133,7 +133,7 @@ let tuple_ref dep n =
 (* Binders. *)
 
 let trad_binder avoid nenv id = function
-  | CC_untyped_binder -> RHole (dummy_loc,AbstractionType (Name id))
+  | CC_untyped_binder -> RHole (dummy_loc,BinderType (Name id))
   | CC_typed_binder ty -> Detyping.detype (Global.env()) avoid nenv ty
 
 let rec push_vars avoid nenv = function
-- 
cgit v1.2.3