diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-31 21:20:35 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-31 21:20:35 +0000 |
| commit | 0d4bde766f7ab5c55d20f848bd9e5c394100f2ce (patch) | |
| tree | b10388c73b6bd440d398778f4eda7747e2b0efd4 /contrib/field/field.ml4 | |
| parent | 00608fac2d8e217232d5f2ddd28a43971bf259b7 (diff) | |
Plus de eqT; message Fail
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3826 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/field/field.ml4')
| -rw-r--r-- | contrib/field/field.ml4 | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index 6f5668b19..97360dab2 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -141,20 +141,13 @@ let field g = Library.check_required_library ["Coq";"field";"Field"]; let ist = { lfun=[]; lmatch=[]; debug=get_debug () } in let typ = constr_of_VConstr (pf_env g) (val_interp ist g - <:tactic< - Match Context With - | [|- (eq ?1 ? ?)] -> ?1 - | [|- (eqT ?1 ? ?)] -> ?1>>) in + <:tactic< Match Context With [|- (eq ?1 ? ?)] -> ?1>>) in let th = VConstr (lookup typ) in (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 + | [|- (eq ?1 ?2 ?3)] -> Field_Gen FT + | _ -> Fail "Field: not an equality">>) g (* Verifies that all the terms have the same type and gives the right theory *) let guess_theory env evc = function |