From 215c4e40280a29546bee30fb35bf95f7fa2186ea Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 15 Apr 2013 16:05:05 +0000
Subject: Checker: get rid of code handling section variables

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16401 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/typeops.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'checker/typeops.ml')

diff --git a/checker/typeops.ml b/checker/typeops.ml
index 7ff99bd935..f22649eb52 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -65,12 +65,6 @@ let judge_of_relative env n =
   with Not_found ->
     error_unbound_rel env n
 
-(* Type of variables *)
-let judge_of_variable env id =
-  try named_type id env
-  with Not_found ->
-    error_unbound_var env id
-
 (* Type of constants *)
 
 let type_of_constant_knowing_parameters env t paramtyps =
@@ -247,7 +241,7 @@ let rec execute env cstr =
 
     | Rel n -> judge_of_relative env n
 
-    | Var id -> judge_of_variable env id
+    | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
 
     | Const c -> judge_of_constant env c
 
-- 
cgit v1.2.3