diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-23 22:40:38 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-23 22:40:38 +0000 |
| commit | 69bf012d0d2a71ed19fc89b31073747f85f9a11d (patch) | |
| tree | 277a73b0eff5e138208150b3301daf786575a1fa /contrib | |
| 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')
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 11 | ||||
| -rw-r--r-- | contrib/field/field.ml4 | 20 |
2 files changed, 18 insertions, 13 deletions
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index fc09cfa69..70596779d 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -578,14 +578,11 @@ GEXTEND Gram tac = Tactic.tactic; "." -> let d = Ast.dynamic (in_prog p) in let str = Ast.str s in - <:ast< (CORRECTNESS $str (VERNACDYN $d) (TACTIC $tac)) >> - - | IDENT "Debug"; IDENT "on"; "." -> <:ast< (PROGDEBUGON) >> + <:ast< (CORRECTNESS $str (VERNACDYN $d) (TACTIC $tac)) >> ] ]; + Pcoq.Vernac_.command: + [ [ IDENT "Debug"; IDENT "on"; "." -> <:ast< (PROGDEBUGON) >> - | IDENT "Debug"; IDENT "off"; "." -> <:ast< (PROGDEBUGOFF) >> - - ] ] - ; + | IDENT "Debug"; IDENT "off"; "." -> <:ast< (PROGDEBUGOFF) >> ] ]; END ;; 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) |