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/inductive.ml | 11 +----------
 1 file changed, 1 insertion(+), 10 deletions(-)

(limited to 'checker/inductive.ml')

diff --git a/checker/inductive.ml b/checker/inductive.ml
index ac9bf415c5..9e1524018d 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -752,16 +752,7 @@ let check_one_fix renv recpos def =
         | (Ind _ | Construct _) ->
             List.iter (check_rec_call renv []) l
 
-        | Var id ->
-            begin
-              match pi2 (lookup_named id renv.env) with
-              | None ->
-                  List.iter (check_rec_call renv []) l
-              | Some c ->
-                  try List.iter (check_rec_call renv []) l
-                  with (FixGuardError _) -> 
-		    check_rec_call renv stack (applist(c,l))
-            end
+        | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
 
 	| Sort _ -> assert (l = [])
 
-- 
cgit v1.2.3