Unification: when matching "?n[...,(C u1..un),...] = C u1..un" keep a

candidate for the possible projection (as was introduced in 8.4beta)
but try also to imitate (as was done before 8.4beta but not done in
8.4beta).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15062 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 5 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 6d7a663bd8..b23ac42116 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1523,6 +1523,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
 	  evdref := evd;
 	  evar'')
     | _ ->
+        progress := true;
 	match
 	  let c,args = decompose_app_vect t in
 	  match kind_of_term c with
@@ -1532,16 +1533,30 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
             (*  possible inversions; we do not treat overlap with a possible *)
             (*  alternative inversion of the subterms of the constructor, etc)*)
 	    (match find_projectable_constructor env evd cstr k args cstr_subst with
-	     | [id] -> Some (mkVar id)
+	     | _::_ as l -> Some (List.map mkVar l)
 	     | _ -> None)
 	  | _ -> None
 	with
-	| Some c -> c
+	| Some l ->
+            let ty = get_type_of env' !evdref t in
+            let candidates =
+              try
+                let t =
+                  map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
+	            imitate envk t in
+                t::l
+              with _ -> l in
+            (match candidates with
+            | [x] -> x
+            | _ ->
+	      let (evd,evar'',ev'') =
+                materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
+              evdref := restrict_evar evd (fst ev'') None (Some candidates);
+              evar'')
 	| None ->
-	  progress := true;
 	  (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *)
-	  map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
-	    imitate envk t in
+	    map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
+	      imitate envk t in
 
   let rhs = whd_beta evd rhs (* heuristic *) in
   let body = imitate (env,0) rhs in