Imported Upstream version 8.2pl2+dfsgupstream/8.2.pl2+dfsg

11 files changed, 133 insertions, 45 deletions

diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index c99884c0..62824670 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: decl_interp.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: decl_interp.ml 12422 2009-10-27 08:42:49Z corbinea $ i*)
 
 open Util
 open Names
@@ -334,7 +334,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
       if List.length params <> expected then
 	errorlabstrm "suppose it is" 
 	  (str "Wrong number of extra arguments: " ++ 
-	     (if expected = 0 then str "none" else int expected) ++ 
+	     (if expected = 0 then str "none" else int expected) ++ spc () ++
 	     str "expected.") in
   let app_ind =
     let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 62a8ddfc..67d1d41a 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_proof_instr.ml 12135 2009-05-20 14:49:23Z herbelin $ *)
+(* $Id: decl_proof_instr.ml 12422 2009-10-27 08:42:49Z corbinea $ *)
 
 open Util
 open Pp
@@ -1161,7 +1161,7 @@ let case_tac params pat_info hyps gls0 =
   let clause = build_dep_clause params pat_info per_info hyps gls0 in
   let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
   let nek = 
-    register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info 
+    register_dep_subcase (id,(List.length params,List.length hyps)) (pf_env gls0) per_info 
       pat_info.pat_pat ek in  
   let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in
     tclTHENS (assert_postpone id clause) 
@@ -1227,6 +1227,7 @@ let hrec_for fix_id per_info gls obj_id =
   let hd2 = applist (mkVar fix_id,args@[obj]) in 
     compose_lam rc (whd_beta gls.sigma hd2)
 
+
 let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
   match tree, objs  with
       Close_patt t,_ ->  
@@ -1235,16 +1236,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
     | Skip_patt (_,t),skipped::next_objs -> 
 	let args0 = push_arg skipped args in
 	  execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls
-    | End_patt (id,nhyps),[] -> 
+    | End_patt (id,(nparams,nhyps)),[] -> 
 	begin
 	  match List.assoc id args with
 	      [None,br_args] -> 
-		let metas = 
-		  list_tabulate (fun n -> mkMeta (succ n)) nhyps in
+		let all_metas = 
+		  list_tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps)  in
+		let param_metas,hyp_metas = list_chop nparams all_metas in
 		  tclTHEN
 		    (tclDO nhrec introf)
 		    (tacnext 
-		       (applist (mkVar id,List.rev_append br_args metas))) gls
+		       (applist (mkVar id,
+				 List.append param_metas 
+				   (List.rev_append br_args hyp_metas)))) gls
 	    | _ -> anomaly "wrong stack size"
 	end
     | Split_patt (ids,ind,br), casee::next_objs ->
@@ -1318,7 +1322,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
     | End_patt (_,_) , _ :: _  -> 
 	anomaly "execute_cases : End of branch with garbage left"
 
-
+let understand_my_constr c gls =
+  let env = pf_env gls in
+  let nc = names_of_rel_context env in
+  let rawc = Detyping.detype false [] nc c in
+  let rec frob = function REvar _ -> RHole (dummy_loc,QuestionMark Expand) | rc ->  map_rawconstr frob rc in
+    Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc)
+
+let set_refine,my_refine =
+let refine = ref (fun (_:open_constr) -> (assert false : tactic) ) in
+((fun tac -> refine:= tac),
+(fun c gls -> 
+   let oc = understand_my_constr c gls in
+     !refine oc gls))
 
 (* end focus/claim *)
 		
@@ -1361,7 +1377,7 @@ let end_tac et2 gls =
 	  | ET_Case_analysis,EK_dep tree ->
 		 execute_cases Anonymous pi 
 		   (fun c -> tclTHENLIST 
-		      [refine c;
+		      [my_refine c;
 		       clear clauses;
 		       justification assumption])
 		   (initial_instance_stack clauses) [pi.per_casee] 0 tree
@@ -1382,7 +1398,7 @@ let end_tac et2 gls =
 			     (fun c ->
 				tclTHENLIST 
 				  [clear [fix_id];
-				   refine c;
+				   my_refine c;
 				   clear clauses;
 				   justification assumption])
 			     (initial_instance_stack clauses) 
diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli
index 877c8047..5f4a0485 100644
--- a/tactics/decl_proof_instr.mli
+++ b/tactics/decl_proof_instr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_proof_instr.mli 11481 2008-10-20 19:23:51Z herbelin $ *)
+(* $Id: decl_proof_instr.mli 12422 2009-10-27 08:42:49Z corbinea $ *)
 
 open Refiner
 open Names
@@ -42,20 +42,20 @@ val execute_cases :
     Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic
 
 val tree_of_pats : 
-  identifier * int -> (Rawterm.cases_pattern*recpath) list list ->
+  identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list ->
   split_tree
 
 val add_branch : 
-  identifier * int -> (Rawterm.cases_pattern*recpath) list list ->
+  identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list ->
   split_tree -> split_tree
 
 val append_branch :
-  identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list ->
+  identifier *(int * int) -> int -> (Rawterm.cases_pattern*recpath) list list ->
   (Names.Idset.t * Decl_mode.split_tree) option ->
   (Names.Idset.t * Decl_mode.split_tree) option
 
 val append_tree :
-  identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list ->
+  identifier * (int * int) -> int -> (Rawterm.cases_pattern*recpath) list list ->
   split_tree -> split_tree
 
 val build_dep_clause :   Term.types Decl_expr.statement list ->
@@ -65,7 +65,7 @@ val build_dep_clause :   Term.types Decl_expr.statement list ->
     Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types
 
 val register_dep_subcase :    
-    Names.identifier * int ->
+    Names.identifier * (int * int) ->
     Environ.env ->
     Decl_mode.per_info ->
     Rawterm.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind
@@ -115,3 +115,4 @@ val init_tree:
      (Names.Idset.t * Decl_mode.split_tree) option) ->
     Decl_mode.split_tree
 
+val set_refine : (Evd.open_constr -> Proof_type.tactic) -> unit
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 58a00419..bf199379 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml 12053 2009-04-06 16:20:42Z msozeau $ *)
+(* $Id: equality.ml 12886 2010-03-27 14:22:00Z herbelin $ *)
 
 open Pp
 open Util
@@ -688,6 +688,16 @@ let minimal_free_rels env sigma (c,cty) =
   else
     (cty',rels')
 
+(* Like the above, but recurse over all the rels found until there are
+   no more rels to be found *)
+let minimal_free_rels_rec env sigma =
+  let rec minimalrec_free_rels_rec prev_rels (c,cty) =
+    let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
+    let combined_rels = Intset.union prev_rels direct_rels in
+    let folder rels i = snd (minimalrec_free_rels_rec rels (c, type_of env sigma (mkRel i)))
+    in (cty, List.fold_left folder combined_rels (Intset.elements (Intset.diff direct_rels prev_rels)))
+  in minimalrec_free_rels_rec Intset.empty
+
 (* [sig_clausal_form siglen ty]
     
    Will explode [siglen] [sigS,sigT ]'s on [ty] (depending on the 
@@ -706,7 +716,7 @@ let minimal_free_rels env sigma (c,cty) =
 
    WARNING: No checking is done to make sure that the 
             sigS(or sigT)'s are actually there.
-          - Only homogenious pairs are built i.e. pairs where all the 
+          - Only homogeneous pairs are built i.e. pairs where all the 
    dependencies are of the same sort
 
    [sig_clausal_form] proceed as follows: the default tuple is
@@ -747,7 +757,12 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 	Evd.existential_opt_value (Evd.evars_of !evdref) 
 	(destEvar ev)
       with
-	| Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+	| Some w ->
+            let w_type = type_of env sigma w in
+            if Evarconv.e_conv env evdref w_type a then
+              applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+            else
+              error "Cannot solve a unification problem."
 	| None -> anomaly "Not enough components to build the dependent tuple"
   in
   let scf = sigrec_clausal_form siglen ty in
@@ -812,7 +827,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
  *)
 
 let make_iterated_tuple env sigma dflt (z,zty) =
-  let (zty,rels) = minimal_free_rels env sigma (z,zty) in
+  let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in
   let sort_of_zty = get_sort_of env sigma zty in
   let sorted_rels = Sort.list (<) (Intset.elements rels) in
   let (tuple,tuplety) =
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 8e517453..4ab40acb 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: hiddentac.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
+(* $Id: hiddentac.ml 13124 2010-06-13 11:09:38Z herbelin $ *)
 
 open Term
 open Proof_type
@@ -83,10 +83,10 @@ let h_simple_induction_destruct isrec h =
 let h_simple_induction = h_simple_induction_destruct true
 let h_simple_destruct = h_simple_induction_destruct false
 
-let h_induction_destruct isrec ev l =
+let h_induction_destruct ev isrec l =
   abstract_tactic (TacInductionDestruct (isrec,ev,List.map (fun (c,e,idl,cl) -> 
     List.map inj_ia c,Option.map inj_open_wb e,idl,cl) l))
-    (induction_destruct ev isrec l)
+    (induction_destruct isrec ev l)
 let h_new_induction ev c e idl cl = h_induction_destruct ev true [c,e,idl,cl]
 let h_new_destruct ev c e idl cl = h_induction_destruct ev false [c,e,idl,cl]
 
@@ -105,7 +105,7 @@ let h_revert l = abstract_tactic (TacRevert l) (revert l)
 
 (* Constructors *)
 let h_left ev l  = abstract_tactic (TacLeft (ev,l)) (left_with_ebindings ev l)
-let h_right ev l = abstract_tactic (TacLeft (ev,l)) (right_with_ebindings ev l)
+let h_right ev l = abstract_tactic (TacRight (ev,l)) (right_with_ebindings ev l)
 let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_ebindings ev l)
 (* Moved to tacinterp because of dependencies in Tacinterp.interp
 let h_any_constructor t =
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 977b602e..af204e77 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inv.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: inv.ml 12410 2009-10-24 17:23:39Z herbelin $ *)
 
 open Pp
 open Util
@@ -291,7 +291,7 @@ let generalizeRewriteIntros tac depids id gls =
 let rec tclMAP_i n tacfun = function
   | [] -> tclDO n (tacfun None)
   | a::l -> 
-      if n=0 then error "Too much names."
+      if n=0 then error "Too many names."
       else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l)
 
 let remember_first_eq id x = if !x = no_move then x := MoveAfter id
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index e798f59a..4cbfa6c2 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: leminv.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: leminv.ml 13126 2010-06-13 11:09:51Z herbelin $ *)
 
 open Pp
 open Util
@@ -291,11 +291,15 @@ let add_inversion_lemma_exn na com comsort bool tac =
 (* ================================= *)
 
 let lemInv id c gls =
+  ignore (pf_get_hyp gls id); (* ensure id exists *)
   try
     let clause = mk_clenv_type_of gls c in
     let clause = clenv_constrain_last_binding (mkVar id) clause in
     Clenvtac.res_pf clause ~allow_K:true gls
   with 
+    | NoSuchBinding ->
+	errorlabstrm ""
+	  (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma."))
     |  UserError (a,b) -> 
 	 errorlabstrm "LemInv" 
 	   (str "Cannot refine current goal with the lemma " ++ 
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 322d25e5..ff3f0887 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refine.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: refine.ml 13129 2010-06-13 14:23:55Z herbelin $ *)
 
 (* JCF -- 6 janvier 1998  EXPERIMENTAL *)
 
@@ -108,6 +108,8 @@ let replace_by_meta env sigma = function
 	| _ -> invalid_arg "Tcc.replace_by_meta (TO DO)" 
         *)
       in
+      if occur_meta ty then
+	error "Unable to manage a dependent metavariable of higher-order type.";
       mkCast (m,DEFAULTcast, ty),[n,ty],[Some th]
 
 exception NoMeta
@@ -189,6 +191,8 @@ let rec compute_metamap env sigma c = match kind_of_term c with
       end
 
   | Case (ci,p,cc,v) ->
+      if occur_meta p then
+       error "Unable to manage a metavariable in the return clause of a match.";
       (* bof... *)
       let nbr = Array.length v in
       let v = Array.append [|p;cc|] v in
@@ -380,3 +384,5 @@ let refine (evd,c) gl =
      complicated to update meta types when passing through a binder *)
   let th = compute_metamap (pf_env gl) evd c in
   tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl
+
+let _ = Decl_proof_instr.set_refine refine (* dirty trick to solve circular dependency *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 71b50b66..5c891c58 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacinterp.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: tacinterp.ml 13130 2010-06-13 18:45:09Z herbelin $ *)
 
 open Constrintern
 open Closure
@@ -1096,7 +1096,9 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
                  match_next_pattern find_next')
               with
                 | PatternMatchingFailure -> apply_one_mhyp_context_rec tl in
-            match_next_pattern (fun () -> match_pat lmatch hyp pat) ()
+            match_next_pattern (fun () ->
+	      let hyp = if b<>None then refresh_universes_strict hyp else hyp in
+	      match_pat lmatch hyp pat) ()
 	| Some patv -> 
 	    match b with
 	    | Some body -> 
@@ -1112,7 +1114,9 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
                         | PatternMatchingFailure ->
                             match_next_pattern_in_body next_in_body' () in
                     match_next_pattern_in_typ 
-                      (fun () -> match_pat lmeta hyp pat) ()
+                      (fun () ->
+			let hyp = refresh_universes_strict hyp in
+			match_pat lmeta hyp pat) ()
                   with PatternMatchingFailure -> apply_one_mhyp_context_rec tl
                 in
                 match_next_pattern_in_body 
@@ -2872,7 +2876,8 @@ let add_tacdef isrec tacl =
 (***************************************************************************)
 (* Other entry points *)
 
-let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x
+let glob_tactic x =
+  Flags.with_option strict_check (intern_tactic (make_empty_glob_sign ())) x
 
 let glob_tactic_env l env x = 
   Flags.with_option strict_check
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0a8b5d01..0a4c0fbe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: tactics.ml 12956 2010-04-20 08:49:15Z herbelin $ *)
 
 open Pp
 open Util
@@ -249,14 +249,51 @@ let change_option occl t = function
     Some id -> change_in_hyp occl t id
   | None -> change_in_concl occl t
 
-let change occl c cls =
+let out_arg = function
+  | ArgVar _ -> anomaly "Unevaluated or_var variable"
+  | ArgArg x -> x
+
+let adjust_clause occl cls =
+  (* warn as much as possible on loss of occurrence information *)
   (match cls, occl with
       ({onhyps=(Some(_::_::_)|None)}
       |{onhyps=Some(_::_);concl_occs=((false,_)|(true,_::_))}),
       Some _ ->
 	error "No occurrences expected when changing several hypotheses."
     | _ -> ());
-  onClauses (change_option occl c) cls
+  (* get at clause from cls if only goal or one hyp specified *)
+  let occl,cls = match occl with
+    | None -> None,cls
+    | Some (occs,c) ->
+	if cls.onhyps=Some[] && occs=all_occurrences then
+	  Some (on_snd (List.map out_arg) cls.concl_occs,c),
+	  {cls with concl_occs=all_occurrences_expr}
+	else
+	  match cls.onhyps with
+	  | Some[(occs',id),l] when 
+	      cls.concl_occs=no_occurrences_expr && occs=all_occurrences -> 
+	      Some (on_snd (List.map out_arg) occs',c),
+	      {cls with onhyps=Some[(all_occurrences_expr,id),l]}
+	  | _ ->
+	      occl,cls in
+  (* check if cls has still specified occs *)
+  if cls.onhyps <> None && 
+    List.exists (fun ((occs,_),_) -> occs <> all_occurrences_expr)
+    (Option.get cls.onhyps)
+    || cls.concl_occs <> all_occurrences_expr && 
+       cls.concl_occs <> no_occurrences_expr
+  then
+    Flags.if_verbose Pp.msg_warning
+      (if cls.onhyps=Some[] then
+	str "Trailing \"at\" modifier not taken into account."
+      else
+	str "\"at\" modifier in clause \"in\" not taken into account.");
+  (* Anticipate on onClauses which removes concl if not at all occs *)
+  if cls.concl_occs=no_occurrences_expr then cls
+  else {cls with concl_occs=all_occurrences_expr}
+
+let change occl c cls =
+  onClauses (change_option occl c) (adjust_clause occl cls)
 
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
 let red_in_concl        = reduct_in_concl (red_product,DEFAULTcast)
@@ -1397,10 +1434,6 @@ let quantify lconstr =
    the left of each x1, ...).
 *)
 
-let out_arg = function
-  | ArgVar _ -> anomaly "Unevaluated or_var variable"
-  | ArgArg x -> x
-
 let occurrences_of_hyp id cls =
   let rec hyp_occ = function
       [] -> None
@@ -2546,6 +2579,7 @@ let induction_tac_felim with_evars indvars scheme gl =
 let apply_induction_in_context isrec hyp0 indsign indvars names induct_tac gl =
   let env = pf_env gl in
   let statlists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in
+  let deps = List.map (fun (id,c,t)-> (id,c,refresh_universes_strict t)) deps in
   let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
   let names = compute_induction_names (Array.length indsign) names in
   let dephyps = List.map (fun (id,_,_) -> id) deps in
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 1729695d..d3e7da6a 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(*i $Id: tauto.ml4 11739 2009-01-02 19:33:19Z herbelin $ i*)
+(*i $Id: tauto.ml4 12955 2010-04-20 08:10:14Z herbelin $ i*)
 
 open Term
 open Hipattern
@@ -20,6 +20,7 @@ open Tacticals
 open Tacinterp
 open Tactics
 open Util
+open Genarg
 
 let assoc_var s ist =
   match List.assoc (Names.id_of_string s) ist.lfun with
@@ -97,18 +98,21 @@ let is_conj ist =
 let flatten_contravariant_conj ist =
   let typ = assoc_var "X1" ist in
   let c = assoc_var "X2" ist in
+  let hyp = assoc_var "id" ist in
   match match_with_conjunction ~strict:strict_in_contravariant_hyp typ with
   | Some (_,args) ->
       let i = List.length args in
       if not binary_mode || i = 2 then 
 	let newtyp = valueIn (VConstr (List.fold_right mkArrow args c)) in
+        let hyp = valueIn (VConstr hyp) in
 	let intros =
 	  iter_tac (List.map (fun _ -> <:tactic< intro >>) args) 
 	  <:tactic< idtac >> in
 	<:tactic<
           let newtyp := $newtyp in
-	  assert newtyp by ($intros; apply id; split; assumption);
-	  clear id
+          let hyp := $hyp in
+          assert newtyp by ($intros; apply hyp; split; assumption);
+          clear hyp
 	>>
       else
 	<:tactic<fail>>
@@ -129,16 +133,19 @@ let is_disj ist =
 let flatten_contravariant_disj ist =
   let typ = assoc_var "X1" ist in
   let c = assoc_var "X2" ist in
+  let hyp = assoc_var "id" ist in
   match match_with_disjunction ~strict:strict_in_contravariant_hyp typ with
   | Some (_,args) ->
       let i = List.length args in
       if not binary_mode || i = 2 then 
+	let hyp = valueIn (VConstr hyp) in
 	iter_tac (list_map_i (fun i arg ->
 	  let typ = valueIn (VConstr (mkArrow arg c)) in
 	  <:tactic< 
             let typ := $typ in
-	    assert typ by (intro; apply id; constructor $i; assumption)
-	  >>) 1 args) <:tactic< clear id >>
+            let hyp := $hyp in
+            assert typ by (intro; apply hyp; constructor $i; assumption)
+          >>) 1 args) <:tactic< let hyp := $hyp in clear hyp >>
       else
 	<:tactic<fail>>
   | _ ->