From 8602460eb7ac815a9f86231b58798083d2a438d7 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 8 Sep 2009 14:49:21 +0000
Subject: 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
---
 pretyping/typeclasses.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index d5f5d6182d..c2f046440e 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
-- 
cgit v1.2.3