From c039e4e618d7da96909d42995eb21074945a3624 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 10 Sep 2000 21:22:57 +0000
Subject: Correction pour make doc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/environ.ml | 18 ++----------------
 1 file changed, 2 insertions(+), 16 deletions(-)

(limited to 'kernel/environ.ml')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 604d0aea36..257cba2b14 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -6,7 +6,7 @@ open Util
 open Names
 open Sign
 open Univ
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Declarations
 open Abstraction
@@ -310,21 +310,7 @@ let make_all_name_different env =
        push_rel (Name id,c,t) newenv)
     env
 
-(* Abstractions. *)
-(*
-let evaluable_abst env = function
-  | DOPN (Abst _,_) -> true
-  | _ -> invalid_arg "evaluable_abst"
-
-let translucent_abst env = function
-  | DOPN (Abst _,_) -> false
-  | _ -> invalid_arg "translucent_abst"
-
-let abst_value env = function
-  | DOPN(Abst sp, args) ->
-      contract_abstraction (lookup_abst sp env) args
-  | _ -> invalid_arg "abst_value"
-*)
+(* Constants *)
 let defined_constant env = function
   | DOPN (Const sp, _) -> is_defined (lookup_constant sp env)
   | _ -> invalid_arg "defined_constant"
-- 
cgit v1.2.3