diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-09 08:40:00 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-09 08:40:00 +0000 |
| commit | 18ffccadd1901e666ea3600263454446f52849d8 (patch) | |
| tree | e7c69b9c82ba2e17ee52e5ff29632c817a76f7b7 /contrib/interface | |
| parent | cd4d18cf0de8e8077a9c141a3e825b7647f03f8e (diff) | |
Ajout Simpl et Change sur des sous-termes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3392 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rwxr-xr-x | contrib/interface/blast.ml | 4 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 6 |
2 files changed, 6 insertions, 4 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index d5715fd3d..153d3f637 100755 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -402,7 +402,7 @@ and my_find_search db_list local_db hdc concl = match t with | Res_pf (term,cl) -> unify_resolve (term,cl) | ERes_pf (_,c) -> (fun gl -> error "eres_pf") - | Give_exact c -> exact_no_check c + | Give_exact c -> exact_check c | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_resolve (term,cl)) @@ -516,7 +516,7 @@ let blast_auto = (free_try default_full_auto) (free_try (my_full_eauto 2))) *) ;; -let blast_simpl = (free_try (reduce Simpl [])) +let blast_simpl = (free_try (reduce (Simpl None) [])) ;; let blast_induction1 = (free_try (tclTHEN (tclTRY intro) diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 1c139ca8e..480293333 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -538,7 +538,8 @@ and xlate_red_tactic = | Red true -> xlate_error "" | Red false -> CT_red | Hnf -> CT_hnf - | Simpl -> CT_simpl + | Simpl None -> CT_simpl + | Simpl (Some c) -> xlate_error "Simpl: TODO" | Cbv flag_list -> let conv_flags, red_ids = get_flag flag_list in CT_cbv (CT_conversion_flag_list conv_flags, red_ids) @@ -649,7 +650,8 @@ and xlate_tac = function | TacExtend (_,"Absurd",[c]) -> CT_absurd (xlate_formula (out_gen rawwit_constr c)) - | TacChange (f, b) -> CT_change (xlate_formula f, xlate_clause b) + | TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b) + | TacChange (_, f, b) -> xlate_error "TODO: Change subterms" | TacExtend (_,"Contradiction",[]) -> CT_contradiction | TacDoubleInduction (AnonHyp n1, AnonHyp n2) -> CT_tac_double (CT_int n1, CT_int n2) |