diff options
| author | herbelin | 2003-04-07 17:42:50 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-07 17:42:50 +0000 |
| commit | ee7a12cadf868f9bd01b6836fb9010450bf352ae (patch) | |
| tree | 3a87f23ad10ea41ffeeceee3baec99c6b4cef7c7 | |
| parent | 4ab520180b7597f8358f9d351151cd73e43858a3 (diff) | |
Mauvaise resolution conflit dans commit precedent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3859 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/field/field.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index c502ea9b01..a277e83043 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -150,7 +150,7 @@ let field g = | Some (eq,t::args) when eq = Coqlib.build_coq_eq_data.Coqlib.eq () -> t | _ -> error "The statement is not built from Leibniz' equality" in let th = VConstr (lookup typ) in - (tac_interp [(id_of_string "FT",th)] [] (get_debug ()) + (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ()) <:tactic< Match Context With [|-(eq ?1 ?2 ?3)] -> Field_Gen FT>>) g (* Verifies that all the terms have the same type and gives the right theory *) |