Procedural: we corrected two errors about the handling of mutcase (the "cases"

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 8d07811ea3333d450caf68f347e39f1b6a1772e6..7937e8b4b4ddbb739ed6fb27bafa82a0b3f7f7ea 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -370,23 +370,11 @@ let change_tac ~where ~with_what =
   select0_tac ~where ~job:(`ChangeWith change)
 ;;
 
-let letin_tac ~where:(_,_,(m,hyp,gp)) ~what:(_,_,w) name =
-  assert(m = None);
-  let where = Some w, [], 
-     match gp with 
-     | None -> Some Ast.Implicit
-     | Some where -> 
-         Some 
-          (List.fold_left 
-           (fun t _ -> 
-              Ast.Binder(`Pi,(Ast.Ident("_",None),Some Ast.UserInput),t)) 
-           where hyp)
-  in
-  block_tac [
-   generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyp);
-   exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit));
-   change_tac ~where:("",0,where) ~with_what:("",0,Ast.Ident (name,None))
-  ]
+let letin_tac ~where ~what:(_,_,w) name =
+ block_tac [
+  select_tac ~where ~job:(`Substexpand 1) true;
+  exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit));
+ ]
 ;;
 
 let apply_tac = exact_tac;;
@@ -522,7 +510,7 @@ let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
  let status,_ =
   List.fold_right2
    (fun (id1,e1) ((id2,e2) as item) (status,ctx) ->
-     assert (id1=id2);
+     assert (id1=id2 || (prerr_endline (id1 ^ " vs " ^ id2); false));
      match e1,e2 with
         `Decl t1, NCic.Decl t2 ->
           let status = eq status ctx t1 t2 in