diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-13 18:19:32 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-13 18:19:32 +0000 |
| commit | 577d275822c7a266f865952bdcf2dd41861b5b21 (patch) | |
| tree | be2d4c0e6a05ef8f43605cba4a4bcb02259ec0c6 /tactics | |
| parent | bc50989dea9a5bd1b4ec891e63d67fd3fd2f9c3e (diff) | |
Debugging of the class_setoid tactic and eauto. Prepare for move from
class_setoid to class_tactics...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10563 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_setoid.ml4 | 9 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 11 |
2 files changed, 16 insertions, 4 deletions
diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4 index 5939f840f..6569afc14 100644 --- a/tactics/class_setoid.ml4 +++ b/tactics/class_setoid.ml4 @@ -88,9 +88,12 @@ let setoid_morphism = lazy (gen_constant ["Classes"; "SetoidClass"] "setoid_morp let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv_refl") let arrow_morphism a b = - mkLambda (Name (id_of_string "A"), a, - mkLambda (Name (id_of_string "B"), b, - mkProd (Anonymous, mkRel 2, mkRel 2))) + if isprop a && isprop b then + Lazy.force impl + else + mkLambda (Name (id_of_string "A"), a, + mkLambda (Name (id_of_string "B"), b, + mkProd (Anonymous, mkRel 2, mkRel 2))) let setoid_refl pars x = applistc (Lazy.force setoid_refl_proj) (pars @ [x]) diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index da477f2a3..effebf331 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -241,15 +241,24 @@ module SearchProblem = struct let success s = (sig_it (fst s.tacres)) = [] + let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) + + let pr_goals gls = + let evars = Evarutil.nf_evars (Refiner.project gls) in + prlist (pr_ev evars) (sig_it gls) + let filter_tactics (glls,v) l = (* let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) +(* let evars = Evarutil.nf_evars (Refiner.project glls) in *) +(* msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *) let rec aux = function | [] -> [] | (tac,pptac) :: tacl -> try let (lgls,ptl) = apply_tac_list tac glls in let v' p = v (ptl p) in -(* msg (hov 0 (pptac ++ str"\n")); *) +(* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) +(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) ((lgls,v'),pptac) :: aux tacl with e when Logic.catchable_exception e -> aux tacl |