diff options
| author | herbelin | 2002-12-09 08:40:00 +0000 |
|---|---|---|
| committer | herbelin | 2002-12-09 08:40:00 +0000 |
| commit | 18ffccadd1901e666ea3600263454446f52849d8 (patch) | |
| tree | e7c69b9c82ba2e17ee52e5ff29632c817a76f7b7 /contrib | |
| 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')
| -rw-r--r-- | contrib/fourier/fourierR.ml | 3 | ||||
| -rwxr-xr-x | contrib/interface/blast.ml | 4 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 6 |
3 files changed, 8 insertions, 5 deletions
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index 1398499cf5..9a2ff4d207 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -357,6 +357,7 @@ let my_cut c gl= let concl = pf_concl gl in apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl ;; + let exact = exact_check;; let tac_use h = match h.htype with @@ -522,7 +523,7 @@ let rec fourier gl= else tac_zero_infeq_false gl (rational_to_fraction cres) in tac:=(tclTHENS (my_cut ineq) - [tclTHEN (change_in_concl + [tclTHEN (change_in_concl None (mkAppL [| parse "not"; ineq|] )) (tclTHEN (apply (if sres then parse "Rnot_lt_lt" diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index d5715fd3d5..153d3f6374 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 1c139ca8ea..4802933337 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) |