- 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

1 files changed, 6 insertions, 8 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 15d33768c..02c517d51 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