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

1 files changed, 7 insertions, 4 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index febfb04947..f9ab283ada 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -216,6 +216,7 @@ let instances r =
     with Not_found -> unbound_class (Global.env()) (loc_of_reference r, id)
 
 let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false)
+let solve_instanciations_problem = ref (fun _ _ -> assert false)
 
 let resolve_typeclass env ev evi (evd, defined as acc) =
   try
@@ -250,7 +251,7 @@ let resolve_one_typeclass_evd env evd types =
 	let evm' = Evd.evars_of evd' in
 	  match Evd.evar_body (Evd.find evm' ev) with
 	      Evar_empty -> raise Not_found
-	    | Evar_defined c -> c
+	    | Evar_defined c -> Evarutil.nf_evar evm' c
       else raise Not_found
   with Exit -> raise Not_found
 
@@ -278,6 +279,8 @@ let destClassApp c =
     | _ -> None
 
 let resolve_typeclasses ?(check=true) env sigma evd =
+(*   try !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) *)
+(*   with _ -> *)
   let evm = Evd.evars_of evd in
   let tc_evars = 
     let f ev evi acc =
@@ -296,14 +299,14 @@ let resolve_typeclasses ?(check=true) env sigma evd =
 	(fun ev evi acc -> 
 	  if (Evd.mem tc_evars ev || not (Evd.mem evm ev)) && evi.evar_body = Evar_empty then
 	    resolve_typeclass env ev evi acc 
-	  else acc) 
+	  else acc)
 	(Evd.evars_of evars) (evars, false) 
     in
       if not progress then evars'
       else
 	sat (Evarutil.nf_evar_defs evars')
-  in sat evd
-
+  in sat (Evarutil.nf_evar_defs evd)
+  
 let class_of_constr c = 
   let extract_ind c =
     match kind_of_term c with