- 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

4 files changed, 37 insertions, 4 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 074dd0901a..c91580044a 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -222,13 +222,24 @@ let dependent_metas clenv mvs conclmetas =
        Metaset.union deps (clenv_metavars clenv.evd mv))
     mvs conclmetas
 
+let duplicated_metas c = 
+  let rec collrec (one,more as acc) c =
+    match kind_of_term c with
+    | Meta mv -> if List.mem mv one then (one,mv::more) else (mv::one,more)
+    | _       -> fold_constr collrec acc c
+  in
+  snd (collrec ([],[]) c)
+
 let clenv_dependent hyps_only clenv =
   let mvs = undefined_metas clenv.evd in
   let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
   let deps = dependent_metas clenv mvs ctyp_mvs in
+  let nonlinear = duplicated_metas (clenv_value clenv) in
+  (* Make the assumption that duplicated metas have internal dependencies *)
   List.filter
-    (fun mv -> Metaset.mem mv deps &&
-               not (hyps_only && Metaset.mem mv ctyp_mvs))
+    (fun mv -> (Metaset.mem mv deps &&
+                not (hyps_only && Metaset.mem mv ctyp_mvs))
+               or List.mem mv nonlinear) 
     mvs
 
 let clenv_missing ce = clenv_dependent true ce
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)
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 73c03097af..4246f0daa5 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -275,6 +275,11 @@ let rec strip_head_cast c = match kind_of_term c with
   | Cast (c,_,_) -> strip_head_cast c
   | _ -> c
 
+(* Get the last arg of an application *)
+let last_arg c = match kind_of_term c with
+  | App (f,cl) -> array_last cl
+  | _ -> anomaly "last_arg"
+
 (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
    subterms of [c]; it carries an extra data [l] (typically a name
    list) which is processed by [g na] (which typically cons [na] to
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index f80deab10c..539951d5c4 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -185,6 +185,9 @@ val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr
 val it_mkProd_or_LetIn_name   : env -> types -> rel_context -> types
 val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
 
+(* Get the last arg of a constr intended to be nn application *)
+val last_arg : constr -> constr
+
 (* name contexts *)
 type names_context = name list
 val add_name : name -> names_context -> names_context