From 70af80aad166bc54e4bbc80dfc9427cfee32aae6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 9 Dec 2008 21:40:22 +0000
Subject: About "apply in":

- Added "simple apply in" (cf wish 1917) + conversion and descent
  under conjunction + contraction of useless beta-redex in "apply in"
  + support for open terms.
- Did not solve the "problem" that "apply in" generates a let-in which
  is type-checked using a kernel conversion in the opposite side of what
  the proof indicated (hence leading to a potential unexpected penalty
  at Qed time).
- When applyng a sequence of lemmas, it would have been nice to allow
  temporary evars as intermediate steps but this was too long to implement.

Smoother API in tactics.mli for assert_by/assert_as/pose_proof.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11662 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/subtac/subtac_utils.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib/subtac')

diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 920b33b7a5..4079b0f200 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -232,7 +232,7 @@ let build_dependent_sum l =
 	  trace (spc () ++ str ("treating evar " ^ string_of_id n));
 	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
 	   with _ -> ());
-	let tac = assert_tac true (Name n) hyptype in
+	let tac = assert_tac (Name n) hyptype in
 	let conttac = 
 	  (fun cont -> 
 	     conttac
-- 
cgit v1.2.3