From 64ac193d372ef8428e85010a862ece55ac011192 Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 27 Jun 2008 15:52:05 +0000 Subject: Enhanced discrimination nets implementation, which can now work with goals containing existentials and use transparency information on constants (optionally). Only used by the typeclasses eauto engine for now, but could be used for other hint bases easily (just switch a boolean). Had to add a new "creation" hint to be able to set said boolean upon creation of the typeclass_instances hint db. Improve the proof-search algorithm for Morphism, up to 10 seconds gained in e.g. Field_theory, Ring_polynom. Added a morphism declaration for [compose]. One needs to declare more constants as being unfoldable using the [Typeclasses unfold] command so that discrimination is done correctly, but that amounts to only 6 declarations in the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11184 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/FSets/FMapFacts.v | 2 ++ theories/FSets/FSetFacts.v | 2 ++ 2 files changed, 4 insertions(+) (limited to 'theories/FSets') diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index e033343d1..20f4623f9 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -660,6 +660,8 @@ Add Relation key E.eq transitivity proved by E.eq_trans as KeySetoid. +Typeclasses unfold key. + Implicit Arguments Equal [[elt]]. Add Parametric Relation (elt : Type) : (t elt) Equal diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index 6afb8fcb7..4d24f54f4 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -309,6 +309,8 @@ Add Relation elt E.eq transitivity proved by E.eq_trans as EltSetoid. +Typeclasses unfold elt. + Add Relation t Equal reflexivity proved by eq_refl symmetry proved by eq_sym -- cgit v1.2.3