diff options
Diffstat (limited to 'plugins/field')
| -rw-r--r-- | plugins/field/field.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index f08ed7db61..4ea9c99b79 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -154,7 +154,7 @@ let field g = | _ -> raise Exit with Hipattern.NoEquationFound | Exit -> error "The statement is not built from Leibniz' equality" in - let th = VConstr (lookup (pf_env g) typ) in + let th = VConstr ([],lookup (pf_env g) typ) in (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ()) <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g @@ -174,8 +174,8 @@ let field_term l g = Coqlib.check_required_library ["Coq";"field";"LegacyField"]; let env = (pf_env g) and evc = (project g) in - let th = valueIn (VConstr (guess_theory env evc l)) - and nl = List.map (fun x -> valueIn (VConstr x)) (Quote.sort_subterm g l) in + let th = valueIn (VConstr ([],guess_theory env evc l)) + and nl = List.map (fun x -> valueIn (VConstr ([],x))) (Quote.sort_subterm g l) in (List.fold_right (fun c a -> let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in |