- Implantation de la suggestion 1873 sur discriminate. Au final,

  discriminate/injection/simplify_eq acceptent maintenant un terme
  comme argument. Les clauses "with" et les variantes "e" sont aussi
  acceptées. Aussi, discriminate sans argument essaie maintenant
  toutes les hyps quantifiées (au lieu de traiter seulement les buts
  t1<>t2).

--This line, and those below, will be ignored--

M    doc/refman/RefMan-tac.tex
M    CHANGES
M    pretyping/evd.ml
M    pretyping/termops.ml
M    pretyping/termops.mli
M    pretyping/clenv.ml
M    tactics/extratactics.ml4
M    tactics/inv.ml
M    tactics/equality.ml
M    tactics/tactics.mli
M    tactics/equality.mli
M    tactics/tacticals.ml
M    tactics/eqdecide.ml4
M    tactics/tacinterp.ml
M    tactics/tactics.ml
M    tactics/extratactics.mli
M    toplevel/auto_ind_decl.ml
M    contrib/funind/invfun.ml
M    test-suite/success/Discriminate.v
M    test-suite/success/Injection.v
M    proofs/clenvtac.mli
M    proofs/clenvtac.ml


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11159 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 2 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 660547b5ce..166114ab63 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -643,6 +643,20 @@ type unsolvability_explanation = SeveralInstancesFound of int
 (**********************************************************)
 (* Pretty-printing *)
 
+let pr_instance_status (sc,typ) =
+  begin match sc with
+  | IsSubType -> str " [or a subtype of it]"
+  | IsSuperType -> str " [or a supertype of it]"
+  | ConvUpToEta 0 -> mt ()
+  | UserGiven -> mt ()
+  | ConvUpToEta n -> str" [or an eta-expansion up to " ++ int n ++ str" of it]"
+  end ++
+  begin match typ with
+  | CoerceToType -> str " [up to coercion]"
+  | TypeNotProcessed -> mt ()
+  | TypeProcessed -> str " [type is checked]"
+  end
+
 let pr_meta_map mmap =
   let pr_name = function
       Name id -> str"[" ++ pr_id id ++ str"]"
@@ -652,10 +666,10 @@ let pr_meta_map mmap =
       	hov 0 
 	  (pr_meta mv ++ pr_name na ++ str " : " ++
            print_constr b.rebus ++ fnl ())
-    | (mv,Clval(na,(b,_),_)) ->
+    | (mv,Clval(na,(b,s),_)) ->
       	hov 0 
 	  (pr_meta mv ++ pr_name na ++ str " := " ++
-           print_constr b.rebus ++ fnl ())
+           print_constr b.rebus ++ spc () ++ pr_instance_status s ++ fnl ())
   in
   prlist pr_meta_binding (metamap_to_list mmap)