-(*
- match t2 with
- | None ->
- let (_,_,t1) = t1 in
- block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
- `JustOne))); clear_volatile_params_tac] status
- | Some t2 ->
- let status,res = are_convertible t1 t2 status goal in
- if res then
- let (_,_,t2) = t2 in
- block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit
- `JustOne))); clear_volatile_params_tac] status
- else
- raise NotEquivalentTypes
-*)