diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-08 14:49:21 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-08 14:49:21 +0000 |
| commit | 8602460eb7ac815a9f86231b58798083d2a438d7 (patch) | |
| tree | 3bf9bef800e066b6e4d550658e7bdf9ff4bf60bd /pretyping | |
| parent | 9922cfb6c2cdd26e09d19a6a9522745868478c10 (diff) | |
Fix the bug-ridden code used to choose leibniz or generalized
rewriting (thanks to Georges Gonthier for pointing it out).
We try to find a declared rewrite relation when the equation does not
look like an equality and otherwise try to reduce it to find a leibniz equality
but don't backtrack on generalized rewriting if this fails. This new
behavior make two fsets scripts fail as they are trying to use an
underlying leibniz equality for a declared rewrite relation, a [red]
fixes it.
Do some renaming from "setoid" to "rewrite".
Fix [is_applied_rewrite_relation]'s bad handling of evars and the
environment.
Fix some [dual] hints in RelationClasses.v and assert that any declared
[Equivalence] can be considered a [RewriteRelation].
Fix minor tex output problem in coqdoc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12310 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typeclasses.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index d5f5d6182..c2f046440 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -84,10 +84,10 @@ val is_class_evar : evar_map -> evar_info -> bool val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> env -> evar_defs -> evar_defs -val resolve_one_typeclass : env -> evar_map -> types -> constr +val resolve_one_typeclass : env -> evar_map -> types -> open_constr val register_add_instance_hint : (constant -> int option -> unit) -> unit val add_instance_hint : constant -> int option -> unit val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref -val solve_instanciation_problem : (env -> evar_map -> types -> constr) ref +val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref |