From 9369925f8edebf18a7d9cc9516521f193117f3f8 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 13 Apr 2011 14:28:32 +0000
Subject: - Remove create_evar_defs - Be careful with
 consider_remaining_unif_problems: it might instantiate an evar, including the
 current goal!

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13995 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/reduction.ml  | 1 -
 kernel/reduction.mli | 2 +-
 2 files changed, 1 insertion(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 8252ffb9ed..c1c7f521a5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -547,4 +547,3 @@ let is_arity env c =
     let _ = dest_arity env c in
     true
   with NotArity -> false
-
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 5256514931..bee8815a25 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -78,5 +78,5 @@ val dest_prod_assum : env -> types -> rel_context * types
 
 exception NotArity
 
-val dest_arity : env -> types -> arity (* raise NotArity if not an arity *)
+val dest_arity : env -> types -> arity (* raises NotArity if not an arity *)
 val is_arity   : env -> types -> bool
-- 
cgit v1.2.3