diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-05 22:56:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-05 22:56:16 +0000 |
| commit | e23f78a6e50cb2ebf1e182ff66f0ca8f6f802ed3 (patch) | |
| tree | fbd5502968492ae3ffc7476b4f8c333e5491817a /tactics/eauto.ml4 | |
| parent | 285ce142bc17fcaea9bc5b73e98f129c5ad3b2d5 (diff) | |
Debugging en syntaxe v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7991 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/eauto.ml4')
| -rw-r--r-- | tactics/eauto.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index fd1f38786..bea6f3303 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -283,7 +283,7 @@ module SearchProblem = struct filter_tactics s.tacres (List.map (fun id -> (e_give_exact_constr (mkVar id), - (str "Exact" ++ spc () ++ pr_id id))) + (str "exact" ++ spc () ++ pr_id id))) (pf_ids_of_hyps g)) in List.map (fun (res,pp) -> { depth = s.depth; tacres = res; @@ -301,7 +301,7 @@ module SearchProblem = struct { depth = s.depth; tacres = res; last_tactic = pp; dblist = s.dblist; localdb = ldb :: List.tl s.localdb }) - (filter_tactics s.tacres [Tactics.intro,(str "Intro")]) + (filter_tactics s.tacres [Tactics.intro,(str "intro")]) in let rec_tacs = let l = |