Add a type argument to letin_tac instead of using casts and recomputing

when one wants a particular type. Rewrite of the unification behind
[Equations], much more robust but still buggy w.r.t. inaccessible
patterns.


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

11 files changed, 295 insertions, 316 deletions

diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4
index d435f51351..020d67f0c5 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/contrib/funind/g_indfun.ml4
@@ -307,7 +307,7 @@ let mkEq typ c1 c2 =
 let poseq_unsafe idunsafe cstr gl =
   let typ = Tacmach.pf_type_of gl cstr in
   tclTHEN
-    (Tactics.letin_tac None (Name idunsafe) cstr allClauses)
+    (Tactics.letin_tac None (Name idunsafe) cstr None allClauses)
     (tclTHENFIRST 
       (Tactics.assert_as true (Util.dummy_loc,IntroAnonymous) (mkEq typ (mkVar idunsafe) cstr)) 
       Tactics.reflexivity)
diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4
index 38009ba81e..6e16d01a9f 100644
--- a/contrib/subtac/equations.ml4
+++ b/contrib/subtac/equations.ml4
@@ -87,7 +87,6 @@ exception Conflict
 let rec pmatch p c =
   match p, c with
   | PRel i, t -> [i, t]
-(*   | PCstr _, PRel i -> [] *)
   | PCstr (c, pl), PCstr (c', pl') when c = c' -> pmatches pl pl'
   | PInac _, _ -> []
   | _, PInac _ -> []
@@ -102,23 +101,22 @@ and pmatches pl l =
       
 let pattern_matches pl l = try Some (pmatches pl l) with Conflict -> None
 
-(* let rec pmatch p c = *)
-(*   match p, kind_of_term c with *)
-(*   | PRel i, t -> true *)
-(*   | t, Rel n -> true *)
-(*   | PCstr (c, pl), App (c', l') when kind_of_term c' = Construct c ->  *)
-(*       pmatches pl (Array.to_list l') *)
-(*   | PCstr (c, []), Construct c' when c' = c -> true *)
-(*   | PInac _, _ -> true *)
-(*   | _, _ -> false *)
-
-(* and pmatches pl l = *)
-(*   match pl, l with *)
-(*   | [], [] -> true *)
-(*   | hd :: tl, hd' :: tl' -> pmatch hd hd' && pmatches tl tl' *)
-(*   | _ -> false *)
-
-(* let pattern_matches pl l = pmatches pl l *)
+let rec pinclude p c =
+  match p, c with
+  | PRel i, t -> true
+  | PCstr (c, pl), PCstr (c', pl') when c = c' -> pincludes pl pl'
+  | PInac _, _ -> true
+  | _, PInac _ -> true
+  | _, _ -> false
+      
+and pincludes pl l =
+  match pl, l with
+  | [], [] -> true
+  | hd :: tl, hd' :: tl' -> 
+      pinclude hd hd' && pincludes tl tl'
+  | _ -> false
+      
+let pattern_includes pl l = pincludes pl l
 
 (** Specialize by a substitution. *)
 
@@ -130,7 +128,7 @@ let subst_rel_subst k s c =
     | Rel n -> 
 	let k = n - depth in 
 	  if k >= 0 then 
-	    try lift depth (assoc k s) 
+	    try lift depth (snd (assoc k s))
 	    with Not_found -> c
 	  else c
     | _ -> map_constr_with_binders succ aux depth c
@@ -175,7 +173,10 @@ and subst_pats env k t = map (subst_pat env k t)
 let rec specialize s p = 
   match p with
   | PRel i -> 
-      if mem_assoc i s then PInac (assoc i s)
+      if mem_assoc i s then
+	let b, t = assoc i s in
+	  if b then PInac t
+	  else PRel (destRel t)
       else p
   | PCstr(c, pl) ->
       PCstr (c, specialize_pats s pl)
@@ -184,6 +185,15 @@ let rec specialize s p =
 and specialize_constr s c = subst_rel_subst 0 s c
 and specialize_pats s = map (specialize s)
 
+let specialize_patterns = function
+  | [] -> fun p -> p
+  | s -> specialize_pats s
+
+let specialize_rel_context s ctx =
+  snd (fold_right (fun (n, b, t) (k, ctx) -> 
+    (succ k, (n, Option.map (subst_rel_subst k s) b, subst_rel_subst k s t) :: ctx))
+	  ctx (0, []))
+    
 let lift_contextn n k sign =
   let rec liftrec k = function
     | (na,c,t)::sign ->
@@ -213,7 +223,7 @@ type splitting =
 and unification_result = 
   rel_context * int * constr * pat * substitution option
 
-and substitution = (int * constr) list
+and substitution = (int * (bool * constr)) list
 
 type problem = identifier * lhs
 
@@ -261,7 +271,7 @@ let split_context n c =
     | hd :: tl -> after, hd, tl
     | [] -> raise (Invalid_argument "split_context")
 	
-let split_tele n ctx =
+let split_tele n (ctx : rel_context) =
   let rec aux after n l =
     match n, l with
     | 0, decl :: before -> before, decl, List.rev after
@@ -327,7 +337,7 @@ let liftn_rel_context n k sign =
 let substnl_rel_context n l =
   map_rel_context_with_binders (fun k -> substnl l (n+k-1))
 
-let reduce_rel_context (ctx : rel_context) (subst : (int * int) list) =
+let reduce_rel_context (ctx : rel_context) (subst : (int * (bool * constr)) list) =
   let _, s, ctx' =
     fold_left (fun (k, s, ctx') (n, b, t as decl) ->
       match b with
@@ -336,112 +346,102 @@ let reduce_rel_context (ctx : rel_context) (subst : (int * int) list) =
       (1, [], []) ctx
   in
   let s = rev s in
-  let s' = map (fun (korig, knew) -> korig, substl s (mkRel knew)) subst in
+  let s' = map (fun (korig, (b, knew)) -> korig, (b, substl s knew)) subst in
     s', ctx'
-    
-(* let substituted_context (subst : (int * constr) list) (ctx : rel_context) = *)
-(*   let substitute_in_ctx n c ctx = *)
-(*     let rec aux k after = function *)
-(*       | [] -> [] *)
-(*       | (name, b, t as decl) :: before -> *)
-(* 	  if k = n then rev after @ (name, Some c, t) :: before *)
-(* 	  else aux (succ k) (decl :: after) before *)
-(*     in aux 1 [] ctx *)
-(*   in *)
-(*   let _, subst =  *)
-(*     fold_left (fun (k, s) _ -> *)
-(*       try let t = assoc k subst in *)
-(* 	    (succ k, (k, (k, t)) :: s) *)
-(*       with Not_found -> *)
-(* 	(succ k, (k, (k, mkRel k)) :: s)) *)
-(*       (1, []) ctx *)
-(*   in *)
-(*   let rec aux ctx' subst' = function *)
-(*     | [] -> ctx', subst' *)
-(*     | (korig, (k, t)) :: rest -> *)
-(* 	if t = mkRel k then  *)
-(* 	  aux ctx' ((korig, k)::subst') rest *)
-(* 	else if noccur_between 0 k t then *)
-(* 	  (\* The term to substitute refers only to previous variables. *\) *)
-(* 	  let t' = lift (-k) t in *)
-(* 	  let ctx' = substitute_in_ctx k t' ctx' in *)
-(* 	    aux ctx' ((korig, k)::subst') rest *)
-(* 	else (\* The term refers to variables declared after [k], so we move [k] *)
-(* 		after them *\) *)
-(* 	  let min = Intset.min_elt (free_rels t) in *)
-(* 	  let before, (n, b, ty), after = split_tele (pred k) ctx' in *)
-(* 	  let afterrest, aftermin = list_chop (pred min) (after : rel_context) in *)
-(* 	  let after' = *)
-(* 	    if dependent_rel_context aftermin 1 then *)
-(* 	      error "Unnable to build a merged context" *)
-(* 	    else substl_rel_context [t] aftermin *)
-(* 	  in *)
-(* 	  let afterrest' = *)
-(* 	    substnl_rel_context (2 + length after') [mkRel min] *)
-(* 	      (liftn_rel_context 2 0 afterrest) *)
-(* 	  in *)
-(* 	  let kdecl' = (n, Some (lift (-min) t), lift (length aftermin) ty) in *)
-(* 	  let ctx' = afterrest' @ (kdecl' :: after') @ before in *)
-(* 	  let substsubst (k', t') = *)
-(* 	    if k' > k then (\* Do nothing *\) (k', t') *)
-(* 	    else  *)
-(* 	      if k' >= min then (succ k, substnl [t] (pred k) t') *)
-(* 	    else *)
-(* 	      (\* Lift to get past the new decl *\) *)
-(* 	      (k, liftn_between 1 0 (length aftermin) t') *)
-(* 	  in  *)
-(* 	  let rest' = map (fun (korig, s) -> korig, substsubst s) rest in *)
-(* 	  let accsubst = map (fun (korig, knew) -> *)
-(* 	    let knew' = *)
-(* 	      if knew > k || knew < min then knew  *)
-(* 	      else if knew = k then min else pred knew  *)
-(* 	    in korig, knew') subst'  *)
-(* 	  in aux ctx' ((korig, min)::accsubst) rest' *)
-(*   in *)
-(*   let ctx', subst' = aux ctx [] subst in *)
-(*     reduce_rel_context ctx' subst' *)
-    
-    
-(*     filter (fun (i, c) -> if isRel c then i <> destRel c else true) *)
-(*       (Array.to_list (Array.mapi (fun i x -> (succ i, x)) recsubst)), ctx' *)
-	
+      
+(* Compute the transitive closure of the dependency relation for a term in a context *)
+
+let rec dependencies_of_rel ctx k =
+  let (n,b,t) = nth ctx (pred k) in
+  let b = Option.map (lift k) b and t = lift k t in
+  let bdeps = match b with Some b -> dependencies_of_term ctx b | None -> Intset.empty in
+    Intset.union (Intset.singleton k) (Intset.union bdeps (dependencies_of_term ctx t))
+      
+and dependencies_of_term ctx t =
+  let rels = free_rels t in
+    Intset.fold (fun i -> Intset.union (dependencies_of_rel ctx i)) rels Intset.empty
 
-let substituted_context subst (ctx : rel_context) =
+let subst_telescope k cstr ctx = 
+  let (_, ctx') = fold_left
+    (fun (k, ctx') (id, b, t) ->
+      (succ k, (id, Option.map (substnl [cstr] k) b, substnl [cstr] k t) :: ctx'))
+    (k, []) ctx
+  in rev ctx'
+
+type ('a,'b) either = Inl of 'a | Inr of 'b
+
+let strengthen (ctx : rel_context) (t : constr) : rel_context * rel_context * (int * (int, int) either) list =
+  let rels = dependencies_of_term ctx t in
+  let len = length ctx in
+  let lifting = len - Intset.cardinal rels in (* Number of variables not linked to t *)
+  let rec aux k n acc m rest s = function
+    | decl :: ctx' ->
+	if Intset.mem k rels then
+	  aux (succ k) (succ n) (decl :: acc) m (subst_telescope 0 (mkRel (succ n + lifting - m)) rest) ((k, Inl n) :: s) ctx'
+	else aux (succ k) n (subst_telescope 0 mkProp acc) (succ m) (decl :: rest) ((k, Inr m) :: s) ctx'
+    | [] -> rev acc, rev rest, s
+  in aux 1 1 [] 1 [] [] ctx
+    
+let merge_subst (ctx', rest, s) =
+  let lenrest = length rest in
+    map (function (k, Inl x) -> (k, (false, mkRel (x + lenrest))) | (k, Inr x) -> k, (false, mkRel x)) s
+
+(* let simplify_subst s =  *)
+(*   fold_left (fun s (k, t) ->  *)
+(*     match kind_of_term t with *)
+(*     | Rel n when n = k -> s *)
+(*     | _ -> (k, t) :: s) *)
+(*     [] s *)
+
+let compose_subst s' s =
+  map (fun (k, (b, t)) -> (k, (b, specialize_constr s' t))) s
+      
+let substituted_context (subst : (int * constr) list) (ctx : rel_context) =
   let substitute_in_ctx n c ctx =
     let rec aux k after = function
       | [] -> []
-      | decl :: before ->
-	  if k = n then subst_rel_context 0 c (rev after) @ before
+      | (name, b, t as decl) :: before ->
+	  if k = n then rev after @ (name, Some c, t) :: before
 	  else aux (succ k) (decl :: after) before
     in aux 1 [] ctx
   in
-  let substitute_in_subst n c s =
-    map (fun (k', c') ->
-      let k' = if k' < n then k' else pred k' in
-	(k', substnl [c] (pred n) c'))
-      s
-  in
-  let recsubst = Array.of_list (list_map_i (fun i _ -> mkRel i) 1 ctx) in
-  let record_subst k t =
-    Array.iteri (fun i c ->
-      if i < k then recsubst.(i) <- substnl [t] k c
-      else if i = k then recsubst.(i) <- t
-      else recsubst.(i) <- lift (-1) c)
-      recsubst
+  let _, subst =
+    fold_left (fun (k, s) _ ->
+      try let t = assoc k subst in
+	    (succ k, (k, (true, t)) :: s)
+      with Not_found ->
+	(succ k, ((k, (false, mkRel k)) :: s)))
+      (1, []) ctx
   in
-  let rec aux ctx' = function
-    | [] -> ctx'
-    | (k, t) :: rest ->
-	let t' = lift (-k) t in
-	let ctx' = substitute_in_ctx k t' ctx' in
-	let rest' = substitute_in_subst k t' rest in
-	  record_subst (pred k) (liftn (-1) k t);
-	  aux ctx' rest'
+  let rec aux ctx' subst' = function
+    | [] -> ctx', subst'
+    | (k, (b, t)) :: rest ->
+	if t = mkRel k then
+	  aux ctx' subst' rest
+	else if noccur_between 0 k t then
+	  (* The term to substitute refers only to previous variables. *)
+	  let t' = lift (-k) t in
+	  let ctx' = substitute_in_ctx k t' ctx' in
+	    aux ctx' subst' rest
+	else (* The term refers to variables declared after [k], so we have 
+		to move these dependencies before [k]. *)
+	  let (minctx, ctxrest, subst as str) = strengthen ctx' t in
+	    match assoc k subst with
+	    | Inl _ -> error "Occurs check in substituted_context"
+	    | Inr k' ->
+		let s = merge_subst str in
+		let ctx' = ctxrest @ minctx in
+		let rest' = 
+		  let substsubst (k', (b, t')) =
+		    match kind_of_term (snd (assoc k' s)) with
+		    | Rel k'' -> (k'', (b, specialize_constr s t'))
+		    | _ -> error "Non-variable substituted for variable by strenghtening"
+		  in map substsubst ((k, (b, t)) :: rest)
+		in aux ctx' (compose_subst s subst') rest'
   in
-  let ctx' = aux ctx subst in
-    filter (fun (i, c) -> if isRel c then i <> destRel c else true)
-      (Array.to_list (Array.mapi (fun i x -> (succ i, x)) recsubst)), ctx'
-	
+  let ctx', subst' = aux ctx subst subst in
+    reduce_rel_context ctx' subst'
+    
 let unify_type before ty =
   try
     let envb = push_rel_context before (Global.env()) in
@@ -476,7 +476,7 @@ let unify_type before ty =
 	  try
 	    let fullenv = push_rel_context fullctx (Global.env ()) in
 	    let vs' = map (lift ctxclen) vs in
-	    let subst = unify_constrs fullenv [] us vs' in
+	    let subst = unify_constrs fullenv [] vs' us in
 	    let subst', ctx' = substituted_context subst fullctx in
 	      (ctx', ctxclen, c, cpat, Some subst')
 	  with Conflict -> 
@@ -533,7 +533,7 @@ and valid_splitting_tree (f, delta, t) = function
 		    subst_context subst (subst_rel_context 0 cstr 
 					    (lift_contextn ctxlen 0 after)) @ before in
 		  let liftpats = lift_pats ctxlen rel lhs in
-		  let newpats = specialize_pats subst (subst_pats (Global.env ()) rel cstrpat liftpats) in
+		  let newpats = specialize_patterns subst (subst_pats (Global.env ()) rel cstrpat liftpats) in
 		    (ok, (f, newdelta, newpats) :: splits))
 	      (true, []) unify
 	  in
@@ -548,15 +548,21 @@ and valid_splitting_tree (f, delta, t) = function
 let valid_tree (f, delta, t) tree = 
   valid_splitting (f, delta, t, patvars_of_tele delta) tree
 
+let is_constructor c =
+  match kind_of_term (fst (decompose_app c)) with
+  | Construct _ -> true
+  | _ -> false
+
 let find_split (_, _, curpats : lhs) (_, _, patcs : lhs) =
   let rec find_split_pat curpat patc =
     match patc with
-    | PRel _ -> (* The pattern's a variable, don't split *) None
+    | PRel _ -> None
     | PCstr (f, args) ->
 	(match curpat with
 	| PCstr (f', args') when f = f' -> (* Already split at this level, continue *)
 	    find_split_pats args' args
 	| PRel i -> (* Split on i *) Some i
+	| PInac c when isRel c -> Some (destRel c)
 	| _ -> None)
     | PInac _ -> None
 
@@ -584,7 +590,11 @@ let pr_pat env c =
   with _ -> str"constr_of_pat raised an exception"
     
 let pr_context env c =
-  let pr_decl (id,b,_) = match id with Name id -> pr_id id | Anonymous -> str"_" in
+  let pr_decl (id,b,_) = 
+    let bstr = match b with Some b -> str ":=" ++ spc () ++ print_constr_env env b | None -> mt() in
+    let idstr = match id with Name id -> pr_id id | Anonymous -> str"_" in
+      idstr ++ bstr
+  in
     prlist_with_sep pr_spc pr_decl (List.rev c)
 (*   Printer.pr_rel_context env c *)
 
@@ -613,8 +623,10 @@ let pr_clause env (lhs, rhs) =
 
 let pr_clauses env =
   prlist_with_sep fnl (pr_clause env)
-    
 
+let lhs_includes (delta, _, patcs : lhs) (delta', _, patcs' : lhs) =
+  pattern_includes patcs patcs'
+    
 let lhs_matches (delta, _, patcs : lhs) (delta', _, patcs' : lhs) =
   pattern_matches patcs patcs'
 
@@ -647,15 +659,15 @@ let rec split_on env var (delta, f, curpats as lhs) clauses =
 	  in
 	  let lifts = (* before; ctxc |- s : newdelta ->
 			 before; ctxc; after |- lifts : newdelta ; after *)
-	    map (fun (k,x) -> (pred var + k, lift (pred var) x)) s
+	    map (fun (k,(b,x)) -> (pred var + k, (b, lift (pred var) x))) s
 	  in
-	  let newpats = specialize_pats lifts substpat in
+	  let newpats = specialize_patterns lifts substpat in
 	  let newlhs = (newdelta, f, newpats) in
 	  let matching, rest = 
 	    fold_right (fun (lhs, rhs as clause) (matching, rest) -> 
-	      match lhs_matches newlhs lhs with
-	      | Some _ -> (clause :: matching, rest)
-	      | None -> (matching, clause :: rest))
+	      if lhs_includes newlhs lhs then
+		(clause :: matching, rest)
+	      else (matching, clause :: rest))
 	      !clauses ([], [])
 	  in
 	    clauses := rest;
@@ -686,9 +698,9 @@ let rec split_on env var (delta, f, curpats as lhs) clauses =
 		Some splitting))
       unify
   in
-    if !clauses <> [] then
-      errorlabstrm "deppat"
-	(str "Impossible clauses:" ++ fnl () ++ pr_clauses env !clauses);
+(*     if !clauses <> [] then *)
+(*       errorlabstrm "deppat" *)
+(* 	(str "Impossible clauses:" ++ fnl () ++ pr_clauses env !clauses); *)
     Split (lhs, var, indf, unify, splits)
       
 and make_split_aux env lhs clauses =
@@ -704,16 +716,15 @@ and make_split_aux env lhs clauses =
 	(match clauses with
 	| [] -> error "No clauses left"
 	| [(lhs', rhs)] ->
-	    Compute (lhs, rhs)
 	    (* No need to split anymore, fix the environments so that they are correctly aligned. *)
-(* 	    (match lhs_matches lhs' lhs with *)
-(* 	    | Some s ->  *)
-(* 		let s = map (fun (x, p) -> x, constr_of_pat ~inacc:false env p) s in *)
-(* 		let rhs' = match rhs with  *)
-(* 		  | Program c -> Program (specialize_constr s c) *)
-(* 		  | Empty i -> Empty (destRel (assoc i s)) *)
-(* 		in Compute ((pi1 lhs, pi2 lhs, specialize_pats s (pi3 lhs')), rhs') *)
-(* 	    | None -> anomaly "Non-matching clauses at a leaf of the splitting tree") *)
+	    (match lhs_matches lhs' lhs with
+	    | Some s ->
+		let s = map (fun (x, p) -> x, (true, constr_of_pat ~inacc:false env p)) s in
+		let rhs' = match rhs with
+		  | Program c -> Program (specialize_constr s c)
+		  | Empty i -> Empty (destRel (snd (assoc i s)))
+		in Compute ((pi1 lhs, pi2 lhs, specialize_patterns s (pi3 lhs')), rhs')
+	    | None -> anomaly "Non-matching clauses at a leaf of the splitting tree")
 	| _ ->
 	    errorlabstrm "make_split_aux"
 	      (str "Overlapping clauses:" ++ fnl () ++ pr_clauses env clauses))
@@ -881,11 +892,28 @@ let equations_tac = lazy
       (TacArg(TacCall(dummy_loc, 
 		     ArgArg(dummy_loc, tactics_tac "equations"), []))))
 
-let define_by_eqs i l t nt eqs =
+let define_by_eqs with_comp i l t nt eqs =
   let env = Global.env () in
   let isevar = ref (create_evar_defs Evd.empty) in
   let (env', sign), impls = interp_context_evars isevar env l in
   let arity = interp_type_evars isevar env' t in
+  let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in
+  let arity = nf_evar (Evd.evars_of !isevar) arity in
+  let arity = 
+    if with_comp then
+      let compid = add_suffix i "_comp" in
+      let ce =
+	{ const_entry_body = it_mkLambda_or_LetIn arity sign;
+	  const_entry_type = None;
+	  const_entry_opaque = false;
+	  const_entry_boxed = false} 
+      in
+      let c =
+	Declare.declare_constant compid (DefinitionEntry ce, IsDefinition Definition)
+      in mkApp (mkConst c, rel_vect 0 (length sign))
+    else arity
+  in
+  let env = Global.env () in
   let ty = it_mkProd_or_LetIn arity sign in
   let data = Command.compute_interning_datas env Constrintern.Recursive [] [i] [ty] [impls] in
   let fixdecls = [(Name i, None, ty)] in
@@ -997,12 +1025,20 @@ let (wit_decl_notation : Genarg.tlevel decl_notation_argtype),
   (rawwit_decl_notation : Genarg.rlevel decl_notation_argtype) =
   Genarg.create_arg "decl_notation"
 
-
+let equations wc i l t nt eqs =
+  try define_by_eqs wc i l t nt eqs
+  with e -> msg (Cerrors.explain_exn e)
 
 VERNAC COMMAND EXTEND Define_equations
 | [ "Equations" ident(i) binders_let2(l) ":" lconstr(t) ":=" deppat_equations(eqs)
       decl_notation(nt) ] ->
-    [ define_by_eqs i l t nt eqs ]
+    [ equations true i l t nt eqs ]
+      END
+
+VERNAC COMMAND EXTEND Define_equations2
+| [ "Equations_nocomp" ident(i) binders_let2(l) ":" lconstr(t) ":=" deppat_equations(eqs)
+      decl_notation(nt) ] ->
+    [ equations false i l t nt eqs ]
 END
     
 let rec int_of_coq_nat c = 
@@ -1036,7 +1072,7 @@ let solve_equations_goal destruct_tac tac gl =
   let dotac = tclDO (succ targ) intro in
   let subtacs = 
     tclTHENS destruct_tac
-      (map (fun (id, br, brt) -> tclTHEN (letin_tac None (Name id) br onConcl) tac) branches)
+      (map (fun (id, br, brt) -> tclTHEN (letin_tac None (Name id) br (Some brt) onConcl) tac) branches)
   in tclTHENLIST [cleantac ; dotac ; subtacs] gl
     
 TACTIC EXTEND solve_equations
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 22e95ef5d8..f5b0355f5a 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -800,7 +800,7 @@ let refresh_hypinfo env sigma hypinfo =
       match c with 
 	| Some c ->
 	    (* Refresh the clausenv to not get the same meta twice in the goal. *)
-	    hypinfo := decompose_setoid_eqhyp cl.env (Evd.evars_of cl.evd) c l2r;
+	    hypinfo := decompose_setoid_eqhyp env (Evd.evars_of cl.evd) c l2r;
 	| _ -> ()
   else ()
 
@@ -1054,7 +1054,7 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
   let sigma = project gl in
   let eq = build_new gl env sigma flags occs hypinfo concl (Some (Lazy.lazy_from_val cstr)) evars 
   in
-    match eq with  
+    match eq with
     | Some (p, (_, _, oldt, newt)) -> 
 	(try 
 	  evars := Typeclasses.resolve_typeclasses env ~split:false ~fail:true !evars;
@@ -1842,7 +1842,7 @@ let rec head_of_constr t =
 TACTIC EXTEND head_of_constr
   [ "head_of_constr" ident(h) constr(c) ] -> [
     let c = head_of_constr c in
-      letin_tac None (Name h) c allHyps
+      letin_tac None (Name h) c None allHyps
   ]
 END
 
@@ -1938,8 +1938,8 @@ let varify_constr_varmap ty def varh c =
 TACTIC EXTEND varify
   [ "varify" ident(varh) ident(h') constr(ty) constr(def) constr(c) ] -> [
     let vars, c' = varify_constr_varmap ty def (mkVar varh) c in
-      tclTHEN (letin_tac None (Name varh) vars allHyps)
-	(letin_tac None (Name h') c' allHyps)
+      tclTHEN (letin_tac None (Name varh) vars None allHyps)
+	(letin_tac None (Name h') c' None allHyps)
   ]
 END
 
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 3b45573f8d..299e3fd17b 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -264,7 +264,7 @@ let add_justification_hyps keep items gls =
       | _ -> 
 	  let id=pf_get_new_id local_hyp_prefix gls in 
 	    keep:=Idset.add id !keep; 
-	    tclTHEN (letin_tac None (Names.Name id) c Tacexpr.nowhere)
+	    tclTHEN (letin_tac None (Names.Name id) c None Tacexpr.nowhere)
               (thin_body [id]) gls in 
     tclMAP add_aux items gls   
 
@@ -811,7 +811,7 @@ let rec build_function args body =
 
 let define_tac id args body gls =
   let t = build_function args body in
-    letin_tac None (Name id) t Tacexpr.nowhere gls
+    letin_tac None (Name id) t None Tacexpr.nowhere gls
 
 (* tactics for reconsider *)
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index cceda72f99..9994bd7848 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1213,8 +1213,8 @@ let subst_one x gl =
       (id,None,_) -> intro_using id
     | (id,Some hval,htyp) ->
         letin_tac None (Name id)
-	  (mkCast(replace_term varx rhs hval,DEFAULTcast,
-	          replace_term varx rhs htyp)) nowhere
+	  (replace_term varx rhs hval)
+	  (Some (replace_term varx rhs htyp)) nowhere
   in
   let need_rewrite = dephyps <> [] || depconcl in
   tclTHENLIST 
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 8313a09475..5e87d432ba 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -75,5 +75,5 @@ let let_evar name typ gls =
   let evd = Evd.create_goal_evar_defs gls.sigma in
   let evd',evar = Evarutil.new_evar evd (pf_env gls) typ in
   Refiner.tclTHEN (Refiner.tclEVARS (evars_of evd'))
-    (Tactics.letin_tac None name evar nowhere) gls
+    (Tactics.letin_tac None name evar None nowhere) gls
  
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 4283720039..1acc4880c1 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -71,7 +71,7 @@ let h_generalize_dep c =
   abstract_tactic (TacGeneralizeDep (inj_open c))(generalize_dep c)
 let h_let_tac b na c cl =
   let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in
-  abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c cl)
+  abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c None cl)
 let h_instantiate n c ido = 
 (Evar_tactics.instantiate n c ido)
   (* abstract_tactic (TacInstantiate (n,c,cls))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2162d891a5..36ec22ee61 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1404,14 +1404,14 @@ let letin_abstract id c occs gl =
     if depdecls = [] then no_move else MoveAfter(pi1(list_last depdecls)) in
   (depdecls,lastlhyp,ccl)
 
-let letin_tac with_eq name c occs gl =
+let letin_tac with_eq name c ty occs gl =
   let id =
     let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in
     if name = Anonymous then fresh_id [] x gl else
       if not (mem_named_context x (pf_hyps gl)) then x else
 	error ("The variable "^(string_of_id x)^" is already declared.") in
   let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in 
-  let t = pf_type_of gl c in
+  let t = match ty with Some t -> t | None -> pf_type_of gl c in
   let newcl,eq_tac = match with_eq with
     | Some (lr,(loc,ido)) ->
       let heq = match ido with
@@ -1618,14 +1618,14 @@ let atomize_param_of_ind (indref,nparams) hyp0 gl =
 	| Var id ->
 	    let x = fresh_id [] id gl in
 	    tclTHEN
-	      (letin_tac None (Name x) (mkVar id) allClauses)
+	      (letin_tac None (Name x) (mkVar id) None allClauses)
 	      (atomize_one (i-1) ((mkVar x)::avoid)) gl
 	| _ ->
 	    let id = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c)
 		       Anonymous in
 	    let x = fresh_id [] id gl in
 	    tclTHEN
-	      (letin_tac None (Name x) c allClauses)
+	      (letin_tac None (Name x) c None allClauses)
 	      (atomize_one (i-1) ((mkVar x)::avoid)) gl
     else 
       tclIDTAC gl
@@ -2558,7 +2558,7 @@ let new_induct_gen isrec with_evars elim (eqname,names) (c,lbind) cls gl =
 	  | _ ->
 	    if cls <> None then Some (false,(dloc,IntroAnonymous)) else None in
 	tclTHEN
-	  (letin_tac with_eq (Name id) c (Option.default allClauses cls))
+	  (letin_tac with_eq (Name id) c None (Option.default allClauses cls))
 	  (induction_with_atomization_of_ind_arg
 	     isrec with_evars elim names (id,lbind)) gl
 
@@ -2592,7 +2592,7 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc gl =
 		let _ = newlc:=id::!newlc in
 		let _ = letids:=id::!letids in
 		tclTHEN 
-		  (letin_tac None (Name id) c allClauses)
+		  (letin_tac None (Name id) c None allClauses)
 		  (atomize_list newl') gl in
   tclTHENLIST 
     [
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d3d353f172..58df7155e7 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -349,7 +349,7 @@ val cut_in_parallel             : constr list -> tactic
 val assert_as : bool -> intro_pattern_expr located -> constr -> tactic
 val forward   : tactic option -> intro_pattern_expr located -> constr -> tactic
 val letin_tac : (bool * intro_pattern_expr located) option -> name -> 
-  constr -> clause -> tactic
+  constr -> types option -> clause -> tactic
 val true_cut                    : name -> constr -> tactic
 val assert_tac                  : bool -> name -> constr -> tactic
 val generalize      : constr list -> tactic
diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v
index f452aeadb8..955ecc93b6 100644
--- a/test-suite/success/Equations.v
+++ b/test-suite/success/Equations.v
@@ -69,12 +69,17 @@ Require Import Bvector.
 Implicit Arguments Vnil [[A]].
 Implicit Arguments Vcons [[A] [n]].
 
+Ltac do_case p ::= destruct p.
+
+Ltac simpl_intros m := (apply m ; auto) || (intro ; simpl_intros m).
+
+Ltac try_intros m ::= 
+  solve [ intros ; unfold Datatypes.id ; refine m || apply m ] || 
+  solve [ unfold Datatypes.id ; simpl_intros m ].
+
 Equations vhead {A n} (v : vector A (S n)) : A := 
 vhead A n (Vcons a v) := a.
 
-Eval compute in (vhead (Vcons 2 (Vcons 1 Vnil))).
-Eval compute in @vhead.
-
 Equations vmap {A B} (f : A -> B) {n} (v : vector A n) : (vector B n) :=
 vmap A B f 0 Vnil := Vnil ;
 vmap A B f (S n) (Vcons a v) := Vcons (f a) (vmap f v).
@@ -83,73 +88,6 @@ Eval compute in (vmap id (@Vnil nat)).
 Eval compute in (vmap id (@Vcons nat 2 _ Vnil)).
 Eval compute in @vmap.
 
-Record vlast_comp (A : Type) (n : nat) (v : vector A (S n)) : Type := { vlast_return : A }.
-
-Class Comp (comp : Type) :=
-  return_type : comp -> Type ; call : Π c : comp, return_type c.
-
-Instance vlast_Comp A n v : Comp (vlast_comp A n v) :=
-  return_type := λ c, A ;
-  call := λ c, vlast_return A n v c.
-
-Ltac ind v := 
-  intros until v ; generalize_eqs_vars v ; induction v ; simplify_dep_elim.
-
-
-Tactic Notation "rec" ident(v) "as" simple_intropattern(p) :=
-  (try intros until v) ; generalize_eqs_vars v ; induction v as p ; simplify_dep_elim ; 
-    simpl_IH_eqs.
-
-Tactic Notation "rec" hyp(v) :=
-  (try intros until v) ; generalize_eqs_vars v ; induction v ; simplify_dep_elim ; 
-    simpl_IH_eqs.
-
-Tactic Notation "case" "*" hyp(v) "as" simple_intropattern(p) :=
-  (try intros until v) ; generalize_eqs_vars v ; destruct v as p ; simplify_dep_elim.
-
-Tactic Notation "case" "*" hyp(v) :=
-  (try intros until v) ; generalize_eqs_vars v ; destruct v ; simplify_dep_elim.
-
-Tactic Notation "=>" constr(v) := 
-  constructor ; 
-    match goal with
-      | [ |- ?T ] => refine (v:T)
-    end.
-
-Ltac make_refls_term c app :=
-  match c with
-    | _ = _ -> ?c' => make_refls_term (app (@refl_equal _ _))
-    | @JMeq _ _ _ _ -> ?c' => make_refls_term (app (@JMeq_refl _ _))
-    | _ => constr:app
-  end.
-
-Ltac make_refls_IH c app :=
-  match c with
-    | Π x : _, ?c' => make_refls_IH (app _)
-    | _ => make_refls_term c app
-  end.
-
-Ltac simpl_IH H :=
-  let ty := type of H in
-    make_refls_IH ty H.
-
-Ltac move_top H :=
-  match reverse goal with [ H' : _ |- _ ] => move H after H' end.
-
-Ltac simplify_dep_elim_hyp H evhyp :=
-  let ev := eval compute in evhyp in
-    subst evhyp ; intros evhyp ; move_top evhyp ; simplify_dep_elim ; 
-      try clear H ; reverse ; intro evhyp ; eapply evhyp.
-
-(* Tactic Notation "strengthen" hyp(H) := *)
-(*   let strhyp := fresh "H'" in *)
-(*   let ty := type of H in *)
-(*     on_last_hyp ltac:(fun id => *)
-(*       reverse ; evar (strhyp:Type) ; intros until id). *)
-
-(*         assert(strhyp -> ty) ; [ simplify_dep_elim_hyp strhyp | intros ]). *)
-
-
 Equations Below_nat (P : nat -> Type) (n : nat) : Type :=
 Below_nat P 0 := unit ;
 Below_nat P (S n) := prod (P n) (Below_nat P n).
@@ -172,14 +110,10 @@ Definition rec_nat (P : nat -> Type) n (step : Π n, Below_nat P n -> P n) : P n
 Fixpoint Below_vector (P : Π A n, vector A n -> Type) A n (v : vector A n) : Type :=
   match v with Vnil => unit | Vcons a n' v' => prod (P A n' v') (Below_vector P A n' v') end.
 
-(* Equations Below_vector (P : Π A n, vector A n -> Type) A n (v : vector A n) : Type := *)
-(* Below_vector P A ?(0) Vnil := unit ; *)
-(* Below_vector P A ?(S n) (Vcons a v) := prod (P A n v) (Below_vector P A n v). *)
-
 Equations below_vector (P : Π A n, vector A n -> Type) A n (v : vector A n)
   (step : Π A n (v : vector A n), Below_vector P A n v -> P A n v) : Below_vector P A n v :=
-below_vector P A 0 Vnil step := tt ;
-below_vector P A (S n) (Vcons a v) step := 
+below_vector P A ?(0) Vnil step := tt ;
+below_vector P A ?(S n) (Vcons a v) step := 
   let rest := below_vector P A n v step in
     (step A n v rest, rest).
 
@@ -214,48 +148,42 @@ Implicit Arguments Below_vector [P A n].
 
 Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
 
-Ltac idify := match goal with [ |- ?T ] => change (id T) end.
-
-(*  induction v as [ | a v']; simplify_dep_elim. *)
-(*   on_last_hyp ltac:(fun id => *)
-(*     let strhyp := fresh "H'" in *)
-(*     let ty := type of IHv in *)
-(*       reverse ; evar (strhyp:Type) ; intros ; *)
-(*         let newhyp := fresh "IHv''" in *)
-(*           assert(ty = strhyp) ; [ idtac (* simplify_dep_elim_hyp IHv strhyp *) | idtac ]). *)
-(* (*         subst strhyp ; intros ; try (apply newhyp in IHv) ]). *) *)
-
-Ltac simpl_rec X :=
-  match type of X with
-    | ?f (?c ?x) =>  
-      let X1 := fresh in
-      let X2 := fresh in
-        hnf in X ; destruct X as [X1 X2] ; simplify_hyp X1
-    | _ => idtac
-  end.
-
-Ltac recur v :=
-  try intros until v ; generalize_eqs_vars v ; reverse ;
-  intros until v ; assert (recv:=rec v) ; simpl in recv ;
-    eapply recv; clear ; simplify_dep_elim.
+(* Equations trans {n} {i j k : fin n} (p : finle i j) (q : finle j k) : finle i k := *)
+(* trans (S n) (fz) j k leqz q := leqz ; *)
+(* trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) := leqs (trans p q). *)
 
-Definition vlast {A} {n} (v : vector A (S n)) : vlast_comp A n v.
-recur v. case* v0. case* v0. => a. simpl_rec X.
-=> (call H).
-Defined.
+(* Obligation Tactic := idtac. *)
+(* Solve Obligations using unfold trans_comp ; equations. *)
+
+(* Next Obligation. intro recc. *)
+(*   info solve_equations (case_last) idtac. *)
+(*   solve_method intro. *)
+(*   clear m_1 ; clear ; simplify_method idtac.  *)
+(*   unfold Datatypes.id. intros. until p. *)
+(*   case_last ; simplify_dep_elim. simpl. *)
+(* ; solve_empty 2. *)
+(*   solve_method intro. *)
   
-Record trans_comp {n:nat} {i j k : fin n} (p : finle i j) (q : finle j k) :=  {
-  return_comp : finle i k }.
 
-Equations trans {n} {i j k : fin n} (p : finle i j) (q : finle j k) : finle i k :=
-trans (S n) fz j k leqz q := leqz ;
-trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) := leqs (trans p q).
+(*   subst m_1 ; clear. *)
+(*   simplify_method idtac. *)
+(*   intros. generalize_eqs p. case p. *)
+(*  solve_empty 2. *)
 
-Lemma trans_eq1 n (j k : fin (S n)) (q : finle j k) : trans leqz q = leqz.
-Proof. intros. simplify_equations ; reflexivity. Qed.
+(*   simplify_dep_elim. unfold Datatypes.id. intros. *)
+(*   apply m_0. *)
+(*   Debug Off. *)
+(*   pose (m_0:=(λ (H : nat) (j k : fin (S H)) (_ : finle j k), leqz) : Π (H : nat) (j k : fin (S H)), finle j k -> finle fz k). *)
+(*   intros. *)
 
-Lemma trans_eq2 n i j k p q : @trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (trans p q).
-Proof. intros. simplify_equations ; reflexivity. Qed.
+(*   solve_method intro. *)
+
+
+(* Lemma trans_eq1 n (j k : fin (S n)) (q : finle j k) : trans leqz q = leqz. *)
+(* Proof. intros. simplify_equations ; reflexivity. Qed. *)
+
+(* Lemma trans_eq2 n i j k p q : @trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (trans p q). *)
+(* Proof. intros. simplify_equations ; reflexivity. Qed. *)
 
 Section Image.
   Context {S T : Type}.
@@ -295,7 +223,7 @@ Eval compute in (foo (uarrow ubool ubool) id).
 
 Inductive foobar : Set := bar | baz.
 
-Equations bla f : bool :=
+Equations bla (f : foobar) : bool :=
 bla bar := true ;
 bla baz := false.
 
@@ -327,16 +255,16 @@ tabulate A 0 f := Vnil ;
 tabulate A (S n) f := Vcons (f fz) (tabulate (f ∘ fs)).
 
 Equations vlast' {A} {n} (v : vector A (S n)) : A :=
-vlast' A 0 (Vcons a Vnil) := a ;
-vlast' A (S n) (Vcons a v) := vlast' v.
+vlast' A ?(0) (@Vcons A a 0 Vnil) := a ;
+vlast' A ?(S n) (@Vcons A a (S n) v) := vlast' v.
 
 Lemma vlast_equation1 A (a : A) : vlast' (Vcons a Vnil) = a.
-Proof. intros. compute ; reflexivity. Qed.
+Proof. intros. simplify_equations. reflexivity. Qed.
 
 Lemma vlast_equation2 A n a v : @vlast' A (S n) (Vcons a v) = vlast' v.
-Proof. intros. compute ; reflexivity. Qed.
+Proof. intros. simplify_equations ; reflexivity. Qed.
 
-Print Assumptions vlast.
+Print Assumptions vlast'.
 Print Assumptions nth. 
 Print Assumptions tabulate. 
 
@@ -346,60 +274,69 @@ vliat A (S n) (Vcons a v) := Vcons a (vliat v).
 
 Eval compute in (vliat (Vcons 2 (Vcons 5 (Vcons 4 Vnil)))).
 
-Equations vapp {A} {n m} (v : vector A n) (w : vector A m) : vector A (n + m) :=
-vapp A 0 m Vnil w := w ;
-vapp A (S n) m (Vcons a v) w := Vcons a (vapp v w).
+Equations vapp' {A} {n m} (v : vector A n) (w : vector A m) : vector A (n + m) :=
+vapp' A ?(0) m Vnil w := w ;
+vapp' A ?(S n) m (Vcons a v) w := Vcons a (vapp' v w).
+
+Eval compute in @vapp'.
+
+Fixpoint vapp {A n m} (v : vector A n) (w : vector A m) : vector A (n + m) :=
+  match v with
+    | Vnil => w
+    | Vcons a n' v' => Vcons a (vapp v' w)
+  end.
 
 Lemma JMeq_Vcons_inj A n m a (x : vector A n) (y : vector A m) : n = m -> JMeq x y -> JMeq (Vcons a x) (Vcons a y).
 Proof. intros until y. simplify_dep_elim. reflexivity. Qed.
 
-Equations NoConfusion_fin (P : Prop) {n : nat} (x y : fin n) : Prop :=
-NoConfusion_fin P ?(S n) fz fz := P -> P ;
-NoConfusion_fin P ?(S n) fz (fs y) := P ;
-NoConfusion_fin P ?(S n) (fs x) fz := P ;
-NoConfusion_fin P ?(S n) (fs x) (fs y) := (x = y -> P) -> P.
+Equations_nocomp NoConfusion_fin (P : Prop) {n : nat} (x y : fin n) : Prop :=
+NoConfusion_fin P (S n) fz fz := P -> P ;
+NoConfusion_fin P (S n) fz (fs y) := P ;
+NoConfusion_fin P (S n) (fs x) fz := P ;
+NoConfusion_fin P (S n) (fs x) (fs y) := (x = y -> P) -> P.
+
+Eval compute in NoConfusion_fin.
+Print Assumptions NoConfusion_fin.
 
 Equations noConfusion_fin P (n : nat) (x y : fin n) (H : x = y) : NoConfusion_fin P x y :=
 noConfusion_fin P (S n) fz fz refl := λ p, p ;
 noConfusion_fin P (S n) (fs x) (fs x) refl := λ p : x = x -> P, p refl.
 
-Equations NoConfusion_vect (P : Prop) {A n} (x y : vector A n) : Prop :=
+Equations_nocomp NoConfusion_vect (P : Prop) {A n} (x y : vector A n) : Prop :=
 NoConfusion_vect P A 0 Vnil Vnil := P -> P ;
 NoConfusion_vect P A (S n) (Vcons a x) (Vcons b y) := (a = b -> x = y -> P) -> P.
 
-(* Equations noConfusion_vect (P : Prop) A n (x y : vector A n) (H : x = y) : NoConfusion_vect P x y := *)
-(* noConfusion_vect P A 0 Vnil Vnil refl := λ p, p ; *)
-(* noConfusion_vect P A (S n) (Vcons a v) (Vcons a v) refl := λ p : a = a -> v = v -> P, p refl refl. *)
+Equations noConfusion_vect (P : Prop) A n (x y : vector A n) (H : x = y) : NoConfusion_vect P x y :=
+noConfusion_vect P A 0 Vnil Vnil refl := λ p, p ;
+noConfusion_vect P A (S n) (Vcons a v) (Vcons a v) refl := λ p : a = a -> v = v -> P, p refl refl.
 
-(* Instance fin_noconf n : NoConfusionPackage (fin n) := *)
-(*   NoConfusion := λ P, Π x y, x = y -> NoConfusion_fin P x y ; *)
-(*   noConfusion := λ P x y, noConfusion_fin P n x y. *)
+Instance fin_noconf n : NoConfusionPackage (fin n) :=
+  NoConfusion := λ P, Π x y, x = y -> NoConfusion_fin P x y ;
+  noConfusion := λ P x y, noConfusion_fin P n x y.
 
-(* Instance vect_noconf A n : NoConfusionPackage (vector A n) := *)
-(*   NoConfusion := λ P, Π x y, x = y -> NoConfusion_vect P x y ; *)
-(*   noConfusion := λ P x y, noConfusion_vect P A n x y. *)
+Instance vect_noconf A n : NoConfusionPackage (vector A n) :=
+  NoConfusion := λ P, Π x y, x = y -> NoConfusion_vect P x y ;
+  noConfusion := λ P x y, noConfusion_vect P A n x y.
 
 Equations fog {n} (f : fin n) : nat :=
 fog (S n) fz := 0 ; fog (S n) (fs f) := S (fog f).
 
-About vapp.
-
 Inductive Split {X : Set}{m n : nat} : vector X (m + n) -> Set :=
   append : Π (xs : vector X m)(ys : vector X n), Split (vapp xs ys).
 
 Implicit Arguments Split [[X]].
 
-Equations split {X : Set}(m n : nat) (xs : vector X (m + n)) : Split m n xs :=
-split X 0    n xs := append Vnil xs ;
-split X (S m) n (Vcons x xs) := 
-  let 'append xs' ys' in Split _ _ vec := split m n xs return Split (S m) n (Vcons x vec) in
-    append (Vcons x xs') ys'.
+(* Equations_nocomp split {X : Set}(m n : nat) (xs : vector X (m + n)) : Split m n xs := *)
+(* split X 0    n xs := append Vnil xs ; *)
+(* split X (S m) n (Vcons x xs) := *)
+(*   let 'append xs' ys' in Split _ _ vec := split m n xs return Split (S m) n (Vcons x vec) in *)
+(*     append (Vcons x xs') ys'. *)
 
-Eval compute in (split 0 1 (vapp Vnil (Vcons 2 Vnil))).
-Eval compute in (split _ _ (vapp (Vcons 3 Vnil) (Vcons 2 Vnil))).
+(* Eval compute in (split 0 1 (vapp Vnil (Vcons 2 Vnil))). *)
+(* Eval compute in (split _ _ (vapp (Vcons 3 Vnil) (Vcons 2 Vnil))). *)
 
-Extraction Inline split_obligation_1 split_obligation_2.
+(* Extraction Inline split_obligation_1 split_obligation_2. *)
 
-Recursive Extraction split.
+(* Recursive Extraction split. *)
 
-Eval compute in @split.
+(* Eval compute in @split. *)
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index d299d9dda6..4b17235f28 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -373,7 +373,7 @@ Ltac simplify_one_dep_elim_term c :=
     | @JMeq ?A ?a ?A ?b -> _ => refine (simplification_heq _ _ _ _ _)
     | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _)
     | eq (existT ?P ?p _) (existT ?P ?p _) -> _ => refine (simplification_existT _ _ _ _ _ _ _)
-    | ?x = ?y -> _ =>
+    | ?x = ?y -> _ => (* variables case *)
       (let hyp := fresh in intros hyp ;
         move dependent hyp before x ;
           generalize dependent x ; refine (solution_left _ _ _ _) ; intros until 0) ||
@@ -384,6 +384,8 @@ Ltac simplify_one_dep_elim_term c :=
     | ?f ?x = ?g ?y -> _ => let H := fresh in intros H ; injection H ; clear H
     | ?t = ?u -> _ => let hyp := fresh in
       intros hyp ; elimtype False ; discriminate
+    | ?x = ?y -> _ => let hyp := fresh in
+      intros hyp ; case hyp ; clear hyp
     | id ?T => fail 1 (* Do not put any part of the rhs in the hyps *)
     | _ => intro
   end.
@@ -442,6 +444,8 @@ Ltac reverse_local :=
 Ltac simpl_apply m := refine m.  (* || apply m || simpl ; apply m. *)
 
 Ltac try_intros m := unfold Datatypes.id ; refine m || apply m.  (* (repeat simpl_apply m || intro). *)
+(* Ltac try_intros m := intros ; unfold Datatypes.id ;  *)
+(*   repeat (apply m ; intro) ; let meth := fresh in pose(meth:=m). *)
 
 (** To solve a goal by inversion on a particular target. *)
 
@@ -456,7 +460,7 @@ Ltac simplify_method tac := repeat (tac || simplify_one_dep_elim) ; reverse_loca
 Ltac solve_method rec :=
   match goal with
     | [ H := ?body : nat |- _ ] => subst H ; clear ; abstract (simplify_method idtac ; solve_empty body)
-    | [ H := ?body |- _ ] => clear H ; simplify_method ltac:(exact body) ; rec ; try_intros body
+    | [ H := [ ?body ] : ?T |- _ ] => clear H ; simplify_method ltac:(exact body) ; rec ; try_intros (body:T)
   end.
 
 (** Impossible cases, by splitting on a given target. *)
@@ -474,11 +478,13 @@ Ltac intro_prototypes :=
     | _ => idtac
   end.
 
+Ltac do_case p := case p ; clear p.
+
 Ltac case_last :=
   match goal with
     | [ p : ?x = ?x |- ?T ] => change (id T) ; revert p ; refine (simplification_K _ x _ _)
     | [ p : ?x = ?y |- ?T ] => change (id T) ; revert p
-    | [ p : _ |- ?T ] => simpl in p ; change (id T) ; generalize_eqs p ; destruct p 
+    | [ p : _ |- ?T ] => simpl in p ; change (id T) ; generalize_eqs p ; do_case p
   end.
 
 Ltac nonrec_equations :=