From d410804226ddeb15ab05af5298502ef29efbd0d8 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 26 Aug 1999 09:58:19 +0000
Subject:  - abstraction  - univers fonctionnels  - erreurs de typage
 maintenant sous forme d'exception,    déclarées dans Type_errors

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

(limited to 'kernel/closure.ml')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index f84b231d10..49be8a1a5d 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -652,14 +652,6 @@ type fconstr = sorts oper freeze
 
 let inject constr = freeze ESID constr
 
-(* trivial printer: prints the equivalent constr of a freeze,
- * just writing a "*" if it is in normal form
- *)
-let prfconstr v =
-  let pv = Printer.pr_term (term_of_freeze v) in
-  if v.norm then [< 'sTR"*"; pv >] else pv
-
-
 (* Remove head lifts, applications and casts *)
 let rec strip_frterm n v stack =
   match v.term with
-- 
cgit v1.2.3