Fix bug #1977 by allowing the [apply] variants to take an [open_constr]

instead of a completely resolved [constr] as input. The propagation of the
evars associated to the lemma is only allowed when the evar flag is on
(i.e. for [eapply]), otherwise they should be resolved by the end of the
application. Should be completely backwards compatible...


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

7 files changed, 78 insertions, 59 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 4e910935a..7b654b74b 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -375,6 +375,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 		 (xlate_formula f, List.map xlate_formula_expl l'))
    | CApp(_, (_,f), l) -> 
        CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
+   | CRecord (_,_,_) -> xlate_error "CRecord: TODO"
    | CCases (_, _, _, [], _) -> assert false
    | CCases (_, _, ret_type, tm::tml, eqns)->
        CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm,
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e9ec90ec3..42d74f9ed 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -724,7 +724,7 @@ let unify_resolve_nodelta (c,clenv) gls =
 let unify_resolve flags (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
   let _ = clenv_unique_resolver false ~flags clenv' gls in  
-  h_apply true false [c,NoBindings] gls
+  h_apply true false [inj_open c,NoBindings] gls
 
 
 (* builds a hint database from a constr signature *)
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 1acc4880c..6498c3542 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -40,7 +40,7 @@ let h_exact_no_check c =
 let h_vm_cast_no_check c = 
   abstract_tactic (TacVmCastNoCheck (inj_open c)) (vm_cast_no_check c)
 let h_apply simple ev cb    =
-  abstract_tactic (TacApply (simple,ev,List.map inj_open_wb cb))
+  abstract_tactic (TacApply (simple,ev,cb))
     (apply_with_ebindings_gen simple ev cb)
 let h_elim ev cb cbo    =
   abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo))
@@ -131,8 +131,8 @@ let h_symmetry c     = abstract_tactic (TacSymmetry c) (intros_symmetry c)
 let h_transitivity c =
   abstract_tactic (TacTransitivity (inj_open c)) (intros_transitivity c)
 
-let h_simplest_apply c  = h_apply false false [c,NoBindings]
-let h_simplest_eapply c = h_apply false true [c,NoBindings]
+let h_simplest_apply c  = h_apply false false [inj_open c,NoBindings]
+let h_simplest_eapply c = h_apply false true [inj_open c,NoBindings]
 let h_simplest_elim c   = h_elim false (c,NoBindings) None
 let h_simplest_case   c = h_case false (c,NoBindings)
 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 8d15f864c..938befa49 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -36,7 +36,7 @@ val h_exact_no_check  : constr -> tactic
 val h_vm_cast_no_check  : constr -> tactic
 
 val h_apply           : advanced_flag -> evars_flag -> 
-                        constr with_ebindings list -> tactic
+  open_constr with_bindings list -> tactic
 
 val h_elim            : evars_flag -> constr with_ebindings ->
                         constr with_ebindings option -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 65082c2ee..be15311b9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -719,52 +719,70 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl =
   goal. If this fails, then the head constant will be unfolded step by
   step. *)
   let concl_nprod = nb_prod (pf_concl gl) in
+  let evm, c = c in
+  let origsigm = gl.sigma in
+  let check_evars sigm =
+    let rest = 
+      Evd.fold (fun ev evi acc -> 
+	if Evd.mem sigm ev && not (Evd.mem origsigm ev) && not (Evd.is_defined sigm ev) then
+	  Evd.add acc ev evi
+	else acc) evm Evd.empty
+    in 
+      if not (rest = Evd.empty) then
+	errorlabstrm "apply" (str"Uninstantiated existential variables: " ++ fnl () ++
+				 pr_evar_map rest)
+  in
   let rec try_main_apply c gl =
-  let thm_ty0 = nf_betaiota (pf_type_of gl c) in
-  let try_apply thm_ty nprod =
-    let n = nb_prod thm_ty - nprod in
-    if n<0 then error "Applied theorem has not enough premisses.";
-    let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
-    Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in
-  try try_apply thm_ty0 concl_nprod
-  with PretypeError _|RefinerError _|UserError _|Failure _ as exn ->
-    let rec try_red_apply thm_ty =
-      try 
-        (* Try to head-reduce the conclusion of the theorem *)
-        let red_thm = try_red_product (pf_env gl) (project gl) thm_ty in
-        try try_apply red_thm concl_nprod
-        with PretypeError _|RefinerError _|UserError _|Failure _ ->
-          try_red_apply red_thm
-      with Redelimination -> 
-        (* Last chance: if the head is a variable, apply may try
-	   second order unification *)
-	try if concl_nprod <> 0 then try_apply thm_ty 0 else raise Exit
-	with PretypeError _|RefinerError _|UserError _|Failure _|Exit ->
-	  if with_destruct then
-	   try
-	    let (mind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-	    match match_with_conjunction (snd (decompose_prod t)) with
-	    | Some _ ->
-	      let n = (mis_constr_nargs mind).(0) in
-	      let sort = elimination_sort_of_goal gl in
-	      let elim = pf_apply make_case_gen gl mind sort in
-	      tclTHENLAST
-		(general_elim with_evars (c,NoBindings) (elim,NoBindings))
-		(tclTHENLIST [
-		  tclDO n intro;
-		  tclLAST_NHYPS n (fun l ->
-		    tclFIRST
-		      (List.map (fun id ->
-			tclTHEN (try_main_apply (mkVar id)) (thin l)) l))
-		]) gl
-	    | None ->
-		raise Exit
-	   with RefinerError _|UserError _|Exit -> raise exn 
-	  else
-	    raise exn
- in
-    try_red_apply thm_ty0 in
-  try_main_apply c gl
+    let thm_ty0 = nf_betaiota (pf_type_of gl c) in
+    let try_apply thm_ty nprod =
+      let n = nb_prod thm_ty - nprod in
+	if n<0 then error "Applied theorem has not enough premisses.";
+	let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
+	let res = Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in
+	  if not with_evars then check_evars (fst res).sigma; 
+	  res
+    in
+      try try_apply thm_ty0 concl_nprod
+      with PretypeError _|RefinerError _|UserError _|Failure _ as exn ->
+	let rec try_red_apply thm_ty =
+	  try 
+            (* Try to head-reduce the conclusion of the theorem *)
+            let red_thm = try_red_product (pf_env gl) (project gl) thm_ty in
+              try try_apply red_thm concl_nprod
+              with PretypeError _|RefinerError _|UserError _|Failure _ ->
+		try_red_apply red_thm
+	  with Redelimination -> 
+            (* Last chance: if the head is a variable, apply may try
+	       second order unification *)
+	    try if concl_nprod <> 0 then try_apply thm_ty 0 else raise Exit
+	    with PretypeError _|RefinerError _|UserError _|Failure _|Exit ->
+	      if with_destruct then
+		try
+		  let (mind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+		    match match_with_conjunction (snd (decompose_prod t)) with
+		    | Some _ ->
+			let n = (mis_constr_nargs mind).(0) in
+			let sort = elimination_sort_of_goal gl in
+			let elim = pf_apply make_case_gen gl mind sort in
+			  tclTHENLAST
+			    (general_elim with_evars (c,NoBindings) (elim,NoBindings))
+			    (tclTHENLIST [
+			      tclDO n intro;
+			      tclLAST_NHYPS n (fun l ->
+				tclFIRST
+				  (List.map (fun id ->
+				    tclTHEN (try_main_apply (mkVar id)) (thin l)) l))
+			    ]) gl
+		    | None ->
+			raise Exit
+		with RefinerError _|UserError _|Exit -> raise exn 
+	      else
+		raise exn
+	in try_red_apply thm_ty0 
+  in
+    if evm = Evd.empty then try_main_apply c gl
+    else
+      tclTHEN (tclEVARS (Evd.merge gl.sigma evm)) (try_main_apply c) gl
 
 let rec apply_with_ebindings_gen b e = function
   | [] ->
@@ -778,13 +796,13 @@ let apply_with_ebindings cb = apply_with_ebindings_gen false false [cb]
 let eapply_with_ebindings cb = apply_with_ebindings_gen false true [cb]
 
 let apply_with_bindings (c,bl) =
-  apply_with_ebindings (c,inj_ebindings bl)
+  apply_with_ebindings (inj_open c,inj_ebindings bl)
 
 let eapply_with_bindings (c,bl) =
-  apply_with_ebindings_gen false true [c,inj_ebindings bl]
+  apply_with_ebindings_gen false true [inj_open c,inj_ebindings bl]
 
 let apply c =
-  apply_with_ebindings (c,NoBindings)
+  apply_with_ebindings (inj_open c,NoBindings)
 
 let apply_list = function 
   | c::l -> apply_with_bindings (c,ImplicitBindings l)
@@ -1009,7 +1027,7 @@ let constructor_tac with_evars expctdnumopt i lbind gl =
     Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
   check_number_of_constructors expctdnumopt i nconstr;
   let cons = mkConstruct (ith_constructor_of_inductive mind i) in
-  let apply_tac = general_apply true false with_evars (cons,lbind) in
+  let apply_tac = general_apply true false with_evars (inj_open cons,lbind) in
   (tclTHENLIST 
      [convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 99f2140dd..b2bd508ce 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -181,15 +181,15 @@ val bring_hyps : named_context -> tactic
 val apply                 : constr      -> tactic
 val apply_without_reduce  : constr      -> tactic
 val apply_list            : constr list -> tactic
-
+  
 val apply_with_ebindings_gen : 
-  advanced_flag -> evars_flag -> constr with_ebindings list -> tactic
+  advanced_flag -> evars_flag -> open_constr with_ebindings list -> tactic
 
 val apply_with_bindings   : constr with_bindings -> tactic
 val eapply_with_bindings  : constr with_bindings -> tactic
 
-val apply_with_ebindings  : constr with_ebindings -> tactic
-val eapply_with_ebindings : constr with_ebindings -> tactic
+val apply_with_ebindings  : open_constr with_ebindings -> tactic
+val eapply_with_ebindings : open_constr with_ebindings -> tactic
 
 val cut_and_apply         : constr -> tactic
 
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 0bd9f95dd..8b4cac5f4 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -34,7 +34,7 @@ Class Unconvertible (A : Type) (a b : A).
 Ltac unconvertible :=
   match goal with
     | |- @Unconvertible _ ?x ?y => conv x y ; fail 1 "Convertible"
-    | |- _ => apply Build_Unconvertible 
+    | |- _ => eapply Build_Unconvertible 
   end.
 
 Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.
\ No newline at end of file