diff options
author | 2001-10-23 22:40:38 +0000 | |
---|---|---|
committer | 2001-10-23 22:40:38 +0000 | |
commit | 69bf012d0d2a71ed19fc89b31073747f85f9a11d (patch) | |
tree | 277a73b0eff5e138208150b3301daf786575a1fa /contrib/field/field.ml4 | |
parent | 174efedc2ee4fce87d94f276a591c2cb9993b2b3 (diff) |
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2136 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/field/field.ml4')
-rw-r--r-- | contrib/field/field.ml4 | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index 61bd3353f..90e87c9df 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -71,8 +71,8 @@ let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth ainv_l = begin (try - Ring.add_theory true true false a None None None aplus amult aone azero (Some aopp) aeq rth - Quote.ConstrSet.empty + Ring.add_theory true true false a None None None aplus amult aone azero + (Some aopp) aeq rth Quote.ConstrSet.empty with | UserError("Add Semi Ring",_) -> ()); let th = mkApp ((constant ["Field_Theory"] "Build_Field_Theory"), [|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in @@ -112,12 +112,20 @@ let field g = let ist = { evc=evc; env=env; lfun=[]; lmatch=[]; goalopt=Some g; debug=get_debug () } in let typ = constr_of_Constr (interp_tacarg ist - <:tactic< + <:tactic< Match Context With - | [|-(eq ?1 ? ?)] -> ?1 - | [|-(eqT ?1 ? ?)] -> ?1>>) in + | [|- (eq ?1 ? ?)] -> ?1 + | [|- (eqT ?1 ? ?)] -> ?1>>) in let th = VArg (Constr (lookup typ)) in - (tac_interp [(id_of_string "FT",th)] [] (get_debug ()) <:tactic<Field_Gen FT>>) g + (tac_interp [(id_of_string "FT",th)] [] (get_debug ()) + <:tactic< + Match Context With + | [|- (eq ?1 ?2 ?3)] -> + Let t = (eqT ?1 ?2 ?3) In + Cut t;[Intro; + (Match Context With + | [id:t |- ?] -> Rewrite id;Reflexivity)|Field_Gen FT] + | [|- (eqT ? ? ?)] -> Field_Gen FT>>) g (* Declaration of Field *) let _ = hide_tactic "Field" (function _ -> field) |