From ff599471c8b037a5033724e54657cfe15d0bd681 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 5 Apr 2008 21:45:09 +0000
Subject: - Retour en arrière sur la capacité du nouvel apply à utiliser les  
 lemmes se terminant par False ou not sur n'importe quelle formule   (cela
 crée trop d'incompatibilités dans les "try apply" etc.); de   toutes façons,
 "contradict" joue presque ce rôle (à ceci près qu'il   ne traverse pas les
 conjonctions) (tactics/tactics.ml). - Quelques corrections sur RIneq.v   - le
  hint Rlt_not_eq avait été oublié dans la phase de restructuration,   -
 davantage de noms canoniques (O -> 0, etc.),   - nouvelle tentative de
 ramener "auto" vers Rle (avec Rle_ge) plutôt     que vers Rge qui est moins
 souvent associé à des hints. - Utilisation du formateur deep_ft pour afficher
 les scripts de preuve afin   d'éviter le besoin d'un "Set Printing Depth"
 (vernacentries.ml). - Suppression de certaines utilisations de l'Anomaly de
 meta_fvalue   qui ne correspondaient pas à des comportements anormaux
 (reductionops.ml).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10760 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/reductionops.ml | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 15d33768ce..02c517d517 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -893,13 +893,12 @@ let is_arity env sigma c =
 
 let meta_value evd mv = 
   let rec valrec mv =
-    try
-      let b,_ = meta_fvalue evd mv in
+    match meta_opt_fvalue evd mv with
+    | Some (b,_) -> 
       instance
         (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
         b.rebus
-    with Anomaly _ | Not_found -> 
-      mkMeta mv
+    | None -> mkMeta mv
   in 
   valrec mv
 
@@ -916,13 +915,12 @@ let nf_meta env c = meta_instance env (mk_freelisted c)
 
 let meta_value evd mv = 
   let rec valrec mv =
-    try
-      let b,_ = meta_fvalue evd mv in
+    match meta_opt_fvalue evd mv with
+    | Some (b,_) ->
       instance
         (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
         b.rebus
-    with Anomaly _ | Not_found -> 
-      mkMeta mv
+    | None -> mkMeta mv
   in 
   valrec mv
 
-- 
cgit v1.2.3