From f2b9dfdfb72abb3b797bd651a5846a7e7c761847 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 21 Jun 2007 17:01:21 +0000
Subject: Correction de plusieurs bugs de l'export XML (utilisation d'un type
 de constante par defaut pour les nouveaux types plutot qu'echouer;
 avertissement plutot qu'echec en cas de foncteur; nommage systematique des
 LetIn -- p.ex. functional induction engendre des LetIn non nommes --;
 branchement de la fonction de normalisation de tete evitant CProp sur Closure
 au lieu de Tacred afin de garantir la f.n. de tete)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9902 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/dischargedhypsmap.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/dischargedhypsmap.ml')

diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index 2a2e69e91..4a28c2fa5 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -31,7 +31,7 @@ let get_discharged_hyps sp =
   try
    Spmap.find sp !discharged_hyps_map
   with Not_found ->
-   anomaly ("No discharged hypothesis for object " ^ string_of_path sp)
+    []
 
 (*s Registration as global tables and rollback. *)
 
-- 
cgit v1.2.3