Merge PR #806: closing bug 5315

3 files changed, 49 insertions, 6 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 15ab396e3..5f6d78359 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -821,8 +821,9 @@ let build_proof
 	  | Fix _ | CoFix _ ->
 	      user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet"))
 
+
 	  | Proj _ -> user_err Pp.(str "Prod")
-	  | Prod _ -> user_err Pp.(str "Prod")
+	  | Prod _ -> do_finalize dyn_infos g
 	  | LetIn _ ->
 	      let new_infos =
 		{ dyn_infos with
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 379c83b24..8555a0b22 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -32,6 +32,14 @@ type binder_type =
 
 type glob_context = (binder_type*glob_constr) list
 
+
+let rec solve_trivial_holes pat_as_term e =
+  match pat_as_term.CAst.v,e.CAst.v with
+  | GHole _,_ -> e
+  | GApp(fp,argsp),GApp(fe,argse) when glob_constr_eq fp fe ->
+       CAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse))
+  | _,_ -> pat_as_term
+                                              
 (*
    compose_glob_context [(bt_1,n_1,t_1);......] rt returns
    b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the
@@ -226,7 +234,12 @@ let combine_lam n t b =
 		      compose_glob_context b.context b.value )
   }
 
-
+let combine_prod2 n t b =
+  {
+    context = [];
+    value = mkGProd(n, compose_glob_context t.context t.value,
+		      compose_glob_context b.context b.value )
+  }
 
 let combine_prod n t b =
   { context = t.context@((Prod n,t.value)::b.context); value = b.value}
@@ -604,7 +617,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	let t_res = build_entry_lc env funnames avoid t in
 	let new_env = raw_push_named (n,None,t) env in
 	let b_res = build_entry_lc new_env funnames avoid b in
-	combine_results (combine_prod n) t_res b_res
+        if List.length t_res.result = 1 && List.length b_res.result = 1
+        then combine_results (combine_prod2 n) t_res b_res
+        else combine_results (combine_prod n) t_res b_res
     | GLetIn(n,v,typ,b) ->
 	(* we first compute the list of constructor
 	   corresponding to the body of the function,
@@ -806,6 +821,12 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		 let typ_as_constr = EConstr.of_constr typ_as_constr in
 		 let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in
 		 let pat_as_term = pattern_to_term pat in
+                 (* removing trivial holes *) 
+                 let pat_as_term = solve_trivial_holes pat_as_term e in 
+                  (* observe (str "those_pattern_preconds" ++ spc () ++ *)
+                  (*            str "pat" ++ spc () ++ pr_glob_constr pat_as_term ++ spc ()++ *)
+                  (*            str "e" ++ spc () ++ pr_glob_constr e ++spc ()++ *)
+                  (*            str "typ_as_constr" ++ spc () ++ pr_lconstr typ_as_constr); *)
 		 List.fold_right
 		   (fun id  acc ->
 		      if Id.Set.mem id this_pat_ids
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 7cb35838c..003bb4e30 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -708,9 +708,6 @@ let expand_as =
   in
   expand_as Id.Map.empty
 
-
-
-           
 (* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution 
  *)
 
@@ -749,6 +746,30 @@ If someone knows how to prevent solved existantial removal in  understand, pleas
               Detyping.detype false [] env ctx (EConstr.of_constr (f c))
            | Evar_empty -> rt (* the hole was not solved : we do nothing *)
        )
+    | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *)
+       (
+         let res = 
+           try (* we scan the new evar map to find the evar corresponding to this hole (by looking the source *)
+             Evd.fold (* to simulate an iter *)
+               (fun _ evi _ ->
+                 match evi.evar_source with
+                 | (loc_evi,BinderType na') ->
+                    if Name.equal na na' && rt.CAst.loc = loc_evi  then raise (Found evi)
+                 | _ -> ()
+               )
+               ctx
+               ();
+             (* the hole was not solved : we do nothing *)
+             rt
+           with Found evi -> (* we found the evar corresponding to this hole *)
+                match evi.evar_body with
+                | Evar_defined c ->
+                   (* we just have to lift the solution in glob_term *)
+                   Detyping.detype false [] env ctx (EConstr.of_constr (f c))
+                | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *)
+         in 
+         res
+       )
     | _ -> Glob_ops.map_glob_constr change rt 
   in
   change rt