From 730836f5f680a068633a202de18a4b586157a85c Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 6 Feb 2008 14:59:08 +0000 Subject: New algorithm to resolve morphisms, after discussion with Nicolas Tabareau: - first pass: generation of the Morphism constraints with metavariables for unspecified relations by one fold over the term. This builds a "respect" proof term for the whole term with holes. - second pass: constraint solving of the evars, taking care of finding a solution for all the evars at once. - third step: normalize proof term by found evars, apply it, done! Works with any relation, currently not as efficient as it could be due to bad handling of evars. Also needs some fine tuning of the instances declared in Morphisms.v that are used during proof search, e.g. using priorities. Reorganize Classes.* accordingly, separating the setoids in Classes.SetoidClass from the general morphisms in Classes.Morphisms and the generally applicable relation theory in Classes.Relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10515 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.common | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Makefile.common') diff --git a/Makefile.common b/Makefile.common index 3ba5fcede..c0537f264 100644 --- a/Makefile.common +++ b/Makefile.common @@ -704,8 +704,8 @@ SETOIDSVO:= theories/Setoids/Setoid_tac.vo theories/Setoids/Setoid_Prop.vo theor UNICODEVO:= theories/Unicode/Utf8.vo -CLASSESVO:= theories/Classes/Init.vo theories/Classes/Relations.vo theories/Classes/SetoidClass.vo \ - theories/Classes/SetoidTactics.vo theories/Classes/SetoidDec.vo +CLASSESVO:= theories/Classes/Init.vo theories/Classes/Relations.vo theories/Classes/Morphisms.vo \ + theories/Classes/SetoidClass.vo theories/Classes/SetoidTactics.vo theories/Classes/SetoidDec.vo THEORIESVO:=\ $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ -- cgit v1.2.3