portage Refine

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

14 files changed, 406 insertions, 64 deletions

diff --git a/.depend b/.depend
index 7da1382981..f569d133a7 100644
--- a/.depend
+++ b/.depend
@@ -31,8 +31,6 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
     kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
-lib/system.cmi: lib/pp.cmi 
-lib/util.cmi: lib/pp.cmi 
 library/declare.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
 library/global.cmi: kernel/declarations.cmi kernel/environ.cmi \
@@ -48,6 +46,8 @@ library/library.cmi: lib/pp.cmi
 library/nametab.cmi: kernel/names.cmi 
 library/redinfo.cmi: kernel/names.cmi kernel/term.cmi 
 library/summary.cmi: kernel/names.cmi 
+lib/system.cmi: lib/pp.cmi 
+lib/util.cmi: lib/pp.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     parsing/pcoq.cmi lib/pp.cmi 
 parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
@@ -157,6 +157,7 @@ tactics/hipattern.cmi: kernel/evd.cmi kernel/names.cmi proofs/pattern.cmi \
 tactics/inv.cmi: parsing/coqast.cmi kernel/names.cmi proofs/tacmach.cmi 
 tactics/nbtermdn.cmi: tactics/btermdn.cmi kernel/generic.cmi \
     proofs/pattern.cmi kernel/term.cmi 
+tactics/refine.cmi: proofs/tacmach.cmi kernel/term.cmi 
 tactics/tacentries.cmi: proofs/proof_type.cmi proofs/tacmach.cmi 
 tactics/tacticals.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/names.cmi \
     proofs/pattern.cmi proofs/proof_type.cmi kernel/reduction.cmi \
@@ -185,11 +186,11 @@ toplevel/record.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi
 toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
     kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
-toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
 toplevel/vernacentries.cmi: kernel/names.cmi kernel/term.cmi \
     toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     proofs/proof_type.cmi 
+toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
 dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi 
@@ -316,30 +317,22 @@ lib/dyn.cmo: lib/util.cmi lib/dyn.cmi
 lib/dyn.cmx: lib/util.cmx lib/dyn.cmi 
 lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi 
 lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi 
-lib/gmap.cmo: lib/gmap.cmi 
-lib/gmap.cmx: lib/gmap.cmi 
 lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi 
 lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi 
+lib/gmap.cmo: lib/gmap.cmi 
+lib/gmap.cmx: lib/gmap.cmi 
 lib/gset.cmo: lib/gset.cmi 
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
 lib/hashcons.cmx: lib/hashcons.cmi 
 lib/options.cmo: lib/util.cmi lib/options.cmi 
 lib/options.cmx: lib/util.cmx lib/options.cmi 
-lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
-lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/pp_control.cmo: lib/pp_control.cmi 
 lib/pp_control.cmx: lib/pp_control.cmi 
+lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
+lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/profile.cmo: lib/system.cmi lib/profile.cmi 
 lib/profile.cmx: lib/system.cmx lib/profile.cmi 
-lib/stamps.cmo: lib/stamps.cmi 
-lib/stamps.cmx: lib/stamps.cmi 
-lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi 
-lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi 
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
-lib/util.cmo: lib/pp.cmi lib/util.cmi 
-lib/util.cmx: lib/pp.cmx lib/util.cmi 
 library/declare.cmo: kernel/declarations.cmi kernel/environ.cmi \
     kernel/evd.cmi kernel/generic.cmi library/global.cmi library/impargs.cmi \
     library/indrec.cmi kernel/inductive.cmi library/lib.cmi \
@@ -416,6 +409,14 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
     library/summary.cmi 
 library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
     library/summary.cmi 
+lib/stamps.cmo: lib/stamps.cmi 
+lib/stamps.cmx: lib/stamps.cmi 
+lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi 
+lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi 
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
+lib/util.cmo: lib/pp.cmi lib/util.cmi 
+lib/util.cmx: lib/pp.cmx lib/util.cmi 
 parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \
     kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi 
 parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \
@@ -734,16 +735,16 @@ proofs/stock.cmx: lib/bij.cmx lib/gmap.cmx lib/gmapl.cmx library/library.cmx \
     kernel/names.cmx lib/pp.cmx lib/util.cmx proofs/stock.cmi 
 proofs/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/closure.cmi \
     parsing/coqast.cmi kernel/environ.cmi kernel/generic.cmi lib/gmap.cmi \
-    library/lib.cmi library/libobject.cmi proofs/macros.cmi kernel/names.cmi \
-    library/nametab.cmi lib/options.cmi proofs/pattern.cmi lib/pp.cmi \
-    proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \
+    library/lib.cmi library/libobject.cmi proofs/logic.cmi proofs/macros.cmi \
+    kernel/names.cmi library/nametab.cmi lib/options.cmi proofs/pattern.cmi \
+    lib/pp.cmi proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \
     library/summary.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
     kernel/term.cmi pretyping/typing.cmi lib/util.cmi proofs/tacinterp.cmi 
 proofs/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/closure.cmx \
     parsing/coqast.cmx kernel/environ.cmx kernel/generic.cmx lib/gmap.cmx \
-    library/lib.cmx library/libobject.cmx proofs/macros.cmx kernel/names.cmx \
-    library/nametab.cmx lib/options.cmx proofs/pattern.cmx lib/pp.cmx \
-    proofs/proof_type.cmx pretyping/rawterm.cmx kernel/sign.cmx \
+    library/lib.cmx library/libobject.cmx proofs/logic.cmx proofs/macros.cmx \
+    kernel/names.cmx library/nametab.cmx lib/options.cmx proofs/pattern.cmx \
+    lib/pp.cmx proofs/proof_type.cmx pretyping/rawterm.cmx kernel/sign.cmx \
     library/summary.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
     kernel/term.cmx pretyping/typing.cmx lib/util.cmx proofs/tacinterp.cmi 
 proofs/tacmach.cmo: parsing/ast.cmi parsing/astterm.cmi library/declare.cmi \
@@ -914,6 +915,18 @@ tactics/nbtermdn.cmx: tactics/btermdn.cmx kernel/generic.cmx lib/gmap.cmx \
     library/libobject.cmx library/library.cmx kernel/names.cmx \
     proofs/pattern.cmx kernel/term.cmx tactics/termdn.cmx lib/util.cmx \
     tactics/nbtermdn.cmi 
+tactics/refine.cmo: parsing/astterm.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/generic.cmi kernel/names.cmi lib/pp.cmi pretyping/pretyping.cmi \
+    parsing/printer.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+    kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
+    tactics/refine.cmi 
+tactics/refine.cmx: parsing/astterm.cmx kernel/environ.cmx kernel/evd.cmx \
+    kernel/generic.cmx kernel/names.cmx lib/pp.cmx pretyping/pretyping.cmx \
+    parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \
+    kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
+    tactics/refine.cmi 
 tactics/tacentries.cmo: proofs/proof_trees.cmi proofs/tacmach.cmi \
     tactics/tacticals.cmi tactics/tactics.cmi tactics/tacentries.cmi 
 tactics/tacentries.cmx: proofs/proof_trees.cmx proofs/tacmach.cmx \
@@ -1092,14 +1105,6 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \
     toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi 
 toplevel/usage.cmo: toplevel/usage.cmi 
 toplevel/usage.cmx: toplevel/usage.cmi 
-toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \
-    lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
-    library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
-    toplevel/vernac.cmi 
-toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
-    lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \
-    library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
-    toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
     pretyping/class.cmi toplevel/command.cmi parsing/coqast.cmi \
     library/declare.cmi toplevel/discharge.cmi kernel/environ.cmi \
@@ -1136,6 +1141,14 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx toplevel/command.cmx \
     parsing/coqast.cmx lib/dyn.cmx toplevel/himsg.cmx kernel/names.cmx \
     lib/options.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
     lib/util.cmx toplevel/vernacinterp.cmi 
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \
+    lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
+    library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+    toplevel/vernac.cmi 
+toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
+    lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \
+    library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
+    toplevel/vernac.cmi 
 contrib/omega/coq_omega.cmo: parsing/ast.cmi proofs/clenv.cmi \
     library/declare.cmi kernel/environ.cmi tactics/equality.cmi \
     kernel/generic.cmi library/global.cmi kernel/inductive.cmi \
diff --git a/.depend.coq b/.depend.coq
index 88deb93a8c..3924f5d7a0 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -82,7 +82,7 @@ theories/Arith/Lt.vo: theories/Arith/Lt.v theories/Arith/Le.vo
 theories/Arith/Le.vo: theories/Arith/Le.v
 theories/Arith/Gt.vo: theories/Arith/Gt.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo
 theories/Arith/Even.vo: theories/Arith/Even.v
-theories/Arith/Euclid_proof.vo: theories/Arith/Euclid_proof.v theories/Arith/Minus.vo theories/Arith/Euclid_def.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo
+theories/Arith/Euclid_proof.vo: theories/Arith/Euclid_proof.v theories/Arith/Plus.vo theories/Arith/Minus.vo theories/Arith/Euclid_def.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo
 theories/Arith/Euclid_def.vo: theories/Arith/Euclid_def.v theories/Arith/Mult.vo
 theories/Arith/EqNat.vo: theories/Arith/EqNat.v
 theories/Arith/Div.vo: theories/Arith/Div.v theories/Arith/Le.vo theories/Arith/Euclid_def.vo theories/Arith/Compare_dec.vo
@@ -91,6 +91,7 @@ theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith.vo theo
 theories/Arith/Compare_dec.vo: theories/Arith/Compare_dec.v theories/Arith/Le.vo theories/Arith/Lt.vo
 theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo
 theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo parsing/g_natsyntax.cmo
+test-suite/tactics/TestRefine.vo: test-suite/tactics/TestRefine.v tactics/Refine.vo theories/Init/Wf.vo theories/Arith/Wf_nat.vo theories/Arith/Compare_dec.vo theories/Arith/Lt.vo
 test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v
 test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v
 contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/Zarith/ZArith.vo theories/Logic/Eqdep_dec.vo
@@ -101,15 +102,17 @@ contrib/ring/Ring_abstract.vo: contrib/ring/Ring_abstract.v contrib/ring/Ring_th
 contrib/ring/Quote.vo: contrib/ring/Quote.v contrib/ring/quote.cmo
 contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
 contrib/omega/Zpower.vo: contrib/omega/Zpower.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo
-contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo
+contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo
 contrib/omega/Zcomplements.vo: contrib/omega/Zcomplements.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
 contrib/omega/Omega.vo: contrib/omega/Omega.v theories/Zarith/ZArith.vo theories/Arith/Minus.vo contrib/omega/omega.cmo contrib/omega/coq_omega.cmo contrib/omega/OmegaSyntax.vo
 contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v
 tactics/Tauto.vo: tactics/Tauto.v
+tactics/Refine.vo: tactics/Refine.v
 tactics/Inv.vo: tactics/Inv.v tactics/Equality.vo
 tactics/Equality.vo: tactics/Equality.v
+tactics/EAuto.vo: tactics/EAuto.v
 syntax/PPTactic.vo: syntax/PPTactic.v
 syntax/PPConstr.vo: syntax/PPConstr.v
 syntax/PPCases.vo: syntax/PPCases.v
 syntax/MakeBare.vo: syntax/MakeBare.v
-states/MakeInitial.vo: states/MakeInitial.v theories/Init/Prelude.vo theories/Init/Logic_Type.vo theories/Init/Logic_TypeSyntax.vo tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo
+states/MakeInitial.vo: states/MakeInitial.v theories/Init/Prelude.vo theories/Init/Logic_Type.vo theories/Init/Logic_TypeSyntax.vo tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo tactics/EAuto.vo tactics/Refine.vo
diff --git a/Makefile b/Makefile
index 5317bb1d02..8e4484a993 100644
--- a/Makefile
+++ b/Makefile
@@ -115,7 +115,7 @@ TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo \
 
 HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo \
             tactics/tauto.cmo tactics/inv.cmo tactics/leminv.cmo \
-            tactics/eauto.cmo
+            tactics/eauto.cmo tactics/refine.cmo
 
 CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \
         contrib/ring/quote.cmo contrib/ring/ring.cmo 
@@ -217,7 +217,8 @@ theories/Init/%.vo: theories/Init/%.v states/barestate.coq
 
 init: $(INITVO)
 
-TACTICSVO=tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo tactics/EAuto.vo
+TACTICSVO=tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo \
+          tactics/EAuto.vo tactics/Refine.vo
 
 tactics/%.vo: $(COQC)
 tactics/%.vo: tactics/%.v states/barestate.coq
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index d41e692339..33325bf0b9 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -588,7 +588,7 @@ let interp_casted_constr1 sigma env lvar lmeta com typ =
     interp_rawconstr_gen sigma env false (List.map (fun x -> string_of_id (fst
       x)) lvar) com
   and rtype=fun lst -> retype_list sigma env lst in 
-  ise_resolve_casted_gen sigma env (rtype lvar) (rtype lmeta) typ c;;
+  ise_resolve_casted_gen true sigma env (rtype lvar) (rtype lmeta) typ c;;
 
 (*
 let dbize_fw  sigma env com = dbize FW sigma env com
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 4bc238c4ce..7c4568af12 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -32,7 +32,7 @@ let print_casts = ref false
 
 (* This governs printing of implicit arguments.  When
    [print_implicits] is on then [print_implicits_explicit_args] tells
-   how jimplicit args are printed. If on, implicit args are printed
+   how implicit args are printed. If on, implicit args are printed
    prefixed by "!" otherwise the function and not the arguments is
    prefixed by "!" *)
 let print_implicits = ref false
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index efbf7594a8..4e658787d0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -493,13 +493,13 @@ let j_apply f env sigma j =
        retourne aussi le nouveau sigma...
 *)
 
-let ise_resolve_casted_gen sigma env lvar lmeta typ c =
+let ise_resolve_casted_gen fail_evar sigma env lvar lmeta typ c =
   let isevars = ref sigma in
   let j = unsafe_fmachine (mk_tycon typ) false isevars [] env lvar lmeta c in
-  (j_apply (fun _ -> process_evars true) env !isevars j).uj_val
+  (j_apply (fun _ -> process_evars fail_evar) env !isevars j).uj_val
 
 let ise_resolve_casted sigma env typ c =
-  ise_resolve_casted_gen sigma env [] [] typ c
+  ise_resolve_casted_gen true sigma env [] [] typ c
 
 (* Raw calls to the inference machine of Trad: boolean says if we must fail
    on unresolved evars, or replace them by Metas; the unsafe_judgment list
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index e19b85247f..eb72b7e00d 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -28,7 +28,7 @@ val ise_resolve2 : 'a evar_map -> env -> (identifier * unsafe_judgment) list ->
   (int * unsafe_judgment) list -> rawconstr -> constr
 
 val ise_resolve_casted_gen :
-  'a evar_map -> env -> (identifier * unsafe_judgment) list ->
+  bool -> 'a evar_map -> env -> (identifier * unsafe_judgment) list ->
     (int * unsafe_judgment) list -> constr -> rawconstr -> constr
 val ise_resolve_casted : 'a evar_map -> env -> constr -> rawconstr -> constr
 
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 4340aa31db..c01a547d6a 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -546,30 +546,38 @@ and bind_interp evc env lfun lmatch goalopt = function
     errorlabstrm "bind_interp" [<'sTR "Not the expected form in binding";
       print_ast x>]
 
-(* Interprets a COMMAND expression *)
+(* Interprets a COMMAND expression (in case of failure, returns Command) *)
 and com_interp (evc,env,lfun,lmatch,goalopt) = function
   | Node(_,"EVAL",[c;rtc]) ->
      let redexp = unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
        rtc)) in
      VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr1 evc env
        (make_subs_list lfun) lmatch c)))
-  | c -> VArg (Constr (interp_constr1 evc env (make_subs_list lfun) lmatch c))
+  | c -> 
+      try
+	VArg (Constr (interp_constr1 evc env (make_subs_list lfun) lmatch c))
+      with e when Logic.catchable_exception e ->
+	VArg (Command c)
 
 (* Interprets a CASTEDCOMMAND expression *)
-and cast_com_interp (evc,env,lfun,lmatch,goalopt) com =
-  match goalopt with
-     Some gl ->
-       (match com with
-          | Node(_,"EVAL",[c;rtc]) ->
-            let redexp = unredexp (unvarg (val_interp
-              (evc,env,lfun,lmatch,goalopt) rtc)) in
-            VArg (Constr ((reduction_of_redexp redexp) env evc
-              (interp_casted_constr1 evc env (make_subs_list lfun) lmatch c
-              (pf_concl gl))))
-          | c ->
-            VArg (Constr (interp_casted_constr1 evc env (make_subs_list lfun)
-              lmatch c (pf_concl gl))))
-    | None ->
+and cast_com_interp (evc,env,lfun,lmatch,goalopt) com = match goalopt with
+  | Some gl ->
+      (match com with
+         | Node(_,"EVAL",[c;rtc]) ->
+             let redexp = 
+	       unredexp (unvarg (val_interp
+				   (evc,env,lfun,lmatch,goalopt) rtc)) 
+	     in
+             VArg (Constr ((reduction_of_redexp redexp) env evc
+			     (interp_casted_constr1 evc env 
+				(make_subs_list lfun) lmatch c (pf_concl gl))))
+         | c ->
+	     try
+               VArg (Constr (interp_casted_constr1 evc env 
+			       (make_subs_list lfun) lmatch c (pf_concl gl)))
+	     with e when Logic.catchable_exception e ->
+	       VArg (Command c))
+  | None ->
       errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">]
 
 and cvt_pattern (evc,env,lfun,lmatch,goalopt) = function
diff --git a/states/MakeInitial.v b/states/MakeInitial.v
index eae6c41598..cfc3f5d2ab 100644
--- a/states/MakeInitial.v
+++ b/states/MakeInitial.v
@@ -5,4 +5,5 @@ Require Export Equality.
 Require Export Tauto.
 Require Export Inv.
 Require Export EAuto.
+Require Export Refine.
 
diff --git a/tactics/Refine.v b/tactics/Refine.v
new file mode 100644
index 0000000000..c230e07ec3
--- /dev/null
+++ b/tactics/Refine.v
@@ -0,0 +1,10 @@
+
+(* $Id$ *)
+
+Declare ML Module "refine".
+
+Grammar tactic simple_tactic :=
+  tcc [ "Refine" constrarg($c) ] -> [(Tcc $c)].
+
+Syntax tactic level 0:
+  tcc [(Tcc $C)] -> ["Refine " $C].
diff --git a/tactics/refine.ml b/tactics/refine.ml
new file mode 100644
index 0000000000..f953d349ef
--- /dev/null
+++ b/tactics/refine.ml
@@ -0,0 +1,290 @@
+
+(* $Id$ *)
+
+(* JCF -- 6 janvier 1998  EXPERIMENTAL *)
+
+(*
+ *  L'idée est, en quelque sorte, d'avoir de "vraies" métavariables
+ *  dans Coq, c'est-à-dire de donner des preuves incomplètes -- mais
+ *  où les trous sont typés -- et que les sous-buts correspondants
+ *  soient engendrés pour finir la preuve.
+ *
+ *  Exemple : 
+ *    J'ai le but
+ *        (x:nat) { y:nat | (minus y x) = x }
+ *    et je donne la preuve incomplète
+ *        [x:nat](exist nat [y:nat]((minus y x)=x) (plus x x) ?)
+ *    ce qui engendre le but
+ *        (minus (plus x x) x)=x
+ *)
+
+(*  Pour cela, on procède de la manière suivante :
+ *
+ *  1. Un terme de preuve incomplet est un terme contenant des variables
+ *     existentielles (XTRA "ISEVAR") i.e. "?" en syntaxe concrète.
+ *     La résolution de ces variables n'est plus nécessairement totale
+ *     (ise_resolve called with fail_evar=false) et les variables
+ *     existentielles restantes sont remplacées par des méta-variables
+ *     castées par leur types (celui est connu : soit donné, soit trouvé
+ *     pendant la phase de résolution).
+ *
+ *  2. On met ensuite le terme "à plat" i.e. on n'autorise des MV qu'au
+ *     permier niveau et pour chacune d'elles, si nécessaire, on donne
+ *     à son tour un terme de preuve incomplet pour la résoudre.
+ *     Exemple: le terme (f a ? [x:nat](e ?)) donne
+ *         (f a ?1 ?2) avec ?2 => [x:nat]?3 et ?3 => (e ?4)
+ *         ?1 et ?4 donneront des buts
+ *
+ *  3. On écrit ensuite une tactique tcc qui engendre les sous-buts
+ *     à partir d'une preuve incomplète.
+ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Tacmach
+open Sign
+open Environ
+open Reduction
+open Typing
+open Tactics
+open Tacticals
+open Printer
+
+type metamap = (int * constr) list
+
+type term_with_holes = TH of constr * metamap * sg_proofs
+and  sg_proofs       = (term_with_holes option) list
+
+(* pour debugger *)
+
+let rec pp_th (TH(c,mm,sg)) =
+  [< 'sTR"TH=[ "; hOV 0 [< prterm c; 'fNL;
+			      (* pp_mm mm; 'fNL; *)
+			   pp_sg sg >] ; 'sTR "]" >]
+and pp_mm l =
+  hOV 0 (prlist_with_sep (fun _ -> [< 'fNL >]) 
+	   (fun (n,c) -> [< 'iNT n; 'sTR" --> "; prterm c >]) l)
+and pp_sg sg =
+  hOV 0 (prlist_with_sep (fun _ -> [< 'fNL >])
+	   (function None -> [< 'sTR"None" >] | Some th -> [< pp_th th >]) sg)
+     
+(*  compute_metamap : constr -> term_with_holes
+ *  réalise le 2. ci-dessus
+ *
+ *  Pour cela, on renvoie une metamap qui indique pour chaque meta-variable
+ *  si elle correspond à un but (None) ou si elle réduite à son tour
+ *  par un terme de preuve incomplet (Some c).
+ *
+ *  On a donc l'INVARIANT suivant : le terme c rendu est "de niveau 1"
+ *  -- i.e. à plat -- et la metamap contient autant d'éléments qu'il y 
+ *  a de meta-variables dans c. On suppose de plus que l'ordre dans la
+ *  metamap correspond à celui des buts qui seront engendrés par le refine.
+ *)
+
+let replace_by_meta env = function
+  | TH (DOP0(Meta _) | DOP2(Cast,DOP0(Meta _),_) as m, mm, sgp) -> m,mm,sgp
+  | (TH (c,mm,_)) as th ->
+      let n = new_meta() in
+      let m = DOP0(Meta n) in
+      (* quand on introduit une mv on calcule son type *)
+      let ty = match c with
+	| DOP2(Lambda,c1,DLAM(Name id,DOP2(Cast,_,ty))) ->
+	    mkNamedProd id c1 ty
+	| DOP2(Lambda,c1,DLAM(Anonymous,DOP2(Cast,_,ty))) ->
+	    mkArrow c1 ty
+	| DOPN((AppL|MutCase _),_) ->
+	    (** let j = ise_resolve true empty_evd mm (gLOB sign) c in **)
+	    Retyping.get_type_of_with_meta env Evd.empty mm c
+	| DOPN(Fix (_,j),v) ->
+	    v.(j) (* en pleine confiance ! *)
+	| _ -> invalid_arg "Tcc.replace_by_meta (TO DO)" 
+      in
+      DOP2(Cast,m,ty),[n,ty],[Some th]
+
+exception NoMeta
+
+let replace_in_array env a =
+  if array_for_all (function (TH (_,_,[])) -> true | _ -> false) a then
+    raise NoMeta;
+  let a' = Array.map (function
+			| (TH (c,mm,[])) -> c,mm,[]
+			| th -> replace_by_meta env th) a 
+  in
+  let v' = Array.map (fun (x,_,_) -> x) a' in
+  let mm = Array.fold_left (@) [] (Array.map (fun (_,x,_) -> x) a') in
+  let sgp = Array.fold_left (@) [] (Array.map (fun (_,_,x) -> x) a') in
+  v',mm,sgp
+    
+let fresh env n =
+  let id = match n with Name x -> x | _ -> id_of_string "_" in
+  next_global_ident_away id (ids_of_sign (var_context env))
+
+let rec compute_metamap env = function
+  (* le terme est directement une preuve *)
+  | DOP0(Sort _)
+  | DOPN((Const _ | Abst _ | MutInd _ | MutConstruct _),_)
+  | VAR _ | Rel _ as c -> TH (c,[],[])
+
+  (* le terme est une mv => un but *)
+  | DOP0(Meta n) as c ->
+      Pp.warning (Printf.sprintf ("compute_metamap: MV(%d) sans type !\n") n);
+      TH (c,[],[None])
+  | DOP2(Cast,DOP0(Meta n),ty) as c -> TH (c,[n,ty],[None])
+
+  (* abstraction => il faut décomposer si le terme dessous n'est pas pur
+   *    attention : dans ce cas il faut remplacer (Rel 1) par (VAR x)
+   *    où x est une variable FRAICHE *)
+  | DOP2(Lambda,c1,DLAM(name,c2)) as c ->
+      let v = fresh env name in
+      (** let tj = ise_resolve_type true empty_evd [] (gLOB sign) c1 in **)
+      let tj = execute_type env Evd.empty c1 in
+      let env' = push_var (v,tj) env in
+      begin match compute_metamap env' (subst1 (VAR v) c2) with
+	(* terme de preuve complet *)
+	| TH (_,_,[]) -> TH (c,[],[])
+	(* terme de preuve incomplet *)    
+	| th ->
+	    let m,mm,sgp = replace_by_meta env' th in
+	    TH (DOP2(Lambda,c1,DLAM(Name v,m)), mm, sgp)
+      end
+
+  (* 4. Application *)
+  | DOPN((AppL|MutCase _) as op,v) as c ->
+      let a = Array.map (compute_metamap env) v in
+      begin
+	try
+	  let v',mm,sgp = replace_in_array env a in TH (DOPN(op,v'),mm,sgp)
+	with NoMeta ->
+	  TH (c,[],[])
+      end
+
+  (* 5. Fix. *)
+  | DOPN(Fix _,_) as c ->
+      let ((ni,i),(ai,fi,v)) = destFix c in
+      let vi = List.rev (List.map (fresh env) fi) in
+      let env' =
+	List.fold_left
+	  (fun env (v,ar) -> push_var (v,execute_type env Evd.empty ar) env)
+	  env
+	  (List.combine vi (Array.to_list ai)) 
+      in
+      let a = Array.map
+		(compute_metamap env')
+		(Array.map (substl (List.map (fun x -> VAR x) vi)) v) 
+      in
+      begin
+	try
+	  let v',mm,sgp = replace_in_array env' a in
+	  let fi' = List.rev (List.map (fun id -> Name id) vi) in
+	  let fix = mkFix ((ni,i),(ai,fi',v')) in
+	  TH (fix,mm,sgp)
+	with NoMeta ->
+	  TH (c,[],[])
+      end
+	      
+  (* Cast. Est-ce bien exact ? *)
+  | DOP2(Cast,c,t) -> compute_metamap env c
+      (*let TH (c',mm,sgp) = compute_metamap sign c in
+	TH (DOP2(Cast,c',t),mm,sgp) *)
+      
+  (* Produit. Est-ce bien exact ? *)
+  | DOP2(Prod,_,_) as c ->
+      if occur_meta c then
+	error "Refine: proof term contains metas in a product"
+      else
+      	TH (c,[],[])
+ 
+  (* Autres cas. *)
+  | _ ->
+      invalid_arg "Tcc.compute_metamap"
+
+
+(*  tcc_aux : term_with_holes -> tactic
+ * 
+ *  Réalise le 3. ci-dessus
+ *)
+
+let rec tcc_aux (TH (c,mm,sgp) as th) gl =
+  match (c,sgp) with
+    (* mv => sous-but : on ne fait rien *)
+    | (DOP0(Meta _) | DOP2(Cast,DOP0(Meta _),_)) , _ ->
+	tclIDTAC gl
+	  
+    (* terme pur => refine *)
+    | _,[] ->
+	refine c gl
+	
+    (* abstraction => intro *)
+    | DOP2(Lambda,_,
+	   DLAM(Name id,(DOP0(Meta _)|DOP2(Cast,DOP0(Meta _),_) as m))) ,_ ->
+	begin match sgp with
+	  | [None] -> introduction id gl
+	  | [Some th] ->
+	      tclTHEN (introduction id) (tcc_aux th) gl
+	  | _ -> invalid_arg "Tcc.tcc_aux (bad length)"
+	end
+	
+    | DOP2(Lambda,_,_),_ ->
+	error "invalid abstraction passed to function tcc_aux !"
+      
+    (* fix => tactique Fix *)
+    | DOPN(Fix _,_) , _ ->
+      	let ((ni,_),(ai,fi,_)) = destFix c in
+	let ids =
+	  List.map (function Name id -> id | _ ->
+		      error "recursive functions must have names !") fi 
+	in
+	tclTHENS
+	  (mutual_fix ids (List.map succ (Array.to_list ni))
+             (List.tl (Array.to_list ai)))
+	  (List.map (function
+		       | None -> tclIDTAC 
+		       | Some th -> tcc_aux th) sgp)
+	  gl
+
+    (* sinon on fait refine du terme puis appels rec. sur les sous-buts.
+     * c'est le cas pour AppL et MutCase. *)
+    | _ ->
+	tclTHENS
+	  (refine c)
+	  (List.map (function None -> tclIDTAC | Some th -> tcc_aux th) sgp)
+	  gl
+
+(* Et finalement la tactique refine elle-même : *)
+
+let refine c gl =
+  let env = pf_env gl in
+  let th = compute_metamap env c in
+  tcc_aux th gl
+
+let refine_tac = Tacmach.hide_constr_tactic "Refine" refine
+
+let my_constr_of_com_casted sigma env com typ = 
+  let rawc = Astterm.interp_rawconstr sigma env com in
+  Printf.printf "ICI\n"; flush stdout;
+  let c = Pretyping.ise_resolve_casted_gen false sigma env [] [] typ rawc in
+  Printf.printf "LA\n"; flush stdout;
+  c
+  (**
+  let cc = mkCast (nf_ise1 sigma c) (nf_ise1 sigma typ) in
+  try (unsafe_machine env sigma cc).uj_val
+  with e -> Stdpp.raise_with_loc (Ast.loc com) e
+  **)
+
+open Proof_type
+
+let dyn_tcc args gl = match args with 
+  | [Command com]  ->
+      let env = pf_env gl in
+      refine
+	(my_constr_of_com_casted (project gl) env com (pf_concl gl)) gl
+  | [Constr c] -> 
+      refine c gl
+  | _ -> assert false
+
+let tcc_tac = hide_tactic "Tcc" dyn_tcc
+
+
diff --git a/tactics/refine.mli b/tactics/refine.mli
new file mode 100644
index 0000000000..0277770374
--- /dev/null
+++ b/tactics/refine.mli
@@ -0,0 +1,8 @@
+
+(* $Id$ *)
+
+open Term
+open Tacmach
+
+val refine : constr -> tactic
+val refine_tac : constr -> tactic
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 6de241d184..a1c86e78f6 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -7,14 +7,14 @@
 
 (* PolyList is loaded, but not exported *)
 (* This allow to "hide" the definitions, functions and theorems of PolyList
- and to see only the ones of ListSet *)
+   and to see only the ones of ListSet *)
+
 Require PolyList.
 
 Implicit Arguments On.
 
 Section first_definitions.
 
-
   Variable A : Set.
   Hypothesis Aeq_dec : (x,y:A){x=y}+{~x=y}.
 
@@ -87,10 +87,14 @@ Section first_definitions.
 
   Proof.
     Unfold set_In.
-    Realizer set_mem.
-    Program_all.
-    Rewrite e; Simpl; Auto with datatypes.
-    Simpl; Unfold not; Intros [Hc1 | Hc2 ]; Auto with datatypes.
+    (*** Realizer set_mem. Program_all. ***)
+    Induction x.
+    Auto.
+    Intros a0 x0 Ha0. Case (Aeq_dec a a0); Intro eq.
+    Rewrite eq; Simpl; Auto with datatypes.
+    Elim Ha0.
+    Auto with datatypes.
+    Right; Simpl; Unfold not; Intros [Hc1 | Hc2 ]; Auto with datatypes.
   Save.
 
   Lemma set_mem_ind : 
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 1129e9af02..9638d4a214 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -386,8 +386,12 @@ Fixpoint nth_ok [n:nat; l:list] : A->bool :=
 
 Lemma nth_in_or_default :
   (n:nat)(l:list)(d:A){(In (nth n l d) l)}+{(nth n l d)=d}.
-Realizer nth_ok.
-Program_all.
+(** Realizer nth_ok. Program_all. **)
+Intros n l d; Generalize n; Induction l; Intro n0.
+Right; Case n0; Trivial.
+Case n0; Simpl.
+Auto.
+Intro n1; Elim (Hrecl n1); Auto.     
 Save.
 
 Lemma nth_S_cons :