debug

Author: Tragicus

pretyping/evarsolve.ml

@@ -25,6 +25,8 @@ open Reductionops
 open Evarutil
 open Pretype_errors
 
+let debug_evarsolve = CDebug.create ~name:"evarsolve" ()
+
 module AllowedEvars = struct
 
   type t =
@@ -1587,7 +1589,7 @@ let instantiate_evar unify flags env evd evk body =
   let flags = { flags with allowed_evars } in
   let evd' = check_evar_instance unify flags env evd evk body in
   let evd' = try
-      let evk' = EConstr.destEvar evd' (fst (EConstr.decompose_app evd' body)) in
+      let evk' = fst (EConstr.destEvar evd' (fst (EConstr.decompose_app evd' body))) in
       if List.mem evk (Evd.shelf evd') then Evd.shelve evd' [evk'] else evd'
     with DestKO -> evd' in
   Evd.define evk body evd'
@@ -1774,6 +1776,7 @@ let rec invert_definition unify flags choose imitate_defs
           let f' = imitate envk f in
           if f' == f && Array.for_all2 (==) args args' then t else EConstr.mkApp (f', args')
         | Some i ->
+          let () = debug_evarsolve (fun () -> Pp.(str "rm argument " ++ int i ++ str " from evar " ++ Termops.pr_existential_key env !evdref (fst (EConstr.destEvar !evdref f)) ++ cut ())) in
           let args, args' = Array.chop (i+1) args in
           let evd, e = Evardefine.evar_absorb_arguments env !evdref (EConstr.destEvar !evdref f) (Array.to_list args) in
           evdref := evd; imitate envk (EConstr.mkApp (EConstr.mkEvar e, args')))