(Spawn  ,29765) EXEC: coqidetop.opt -main-channel stdfds --xml_format=Ppcmds -async-proofs on -debug
(Spawn  ,29765) PID 29770
[DEBUG] Start eval_call Init None
[DEBUG] End eval_call
(Spawn  ,29770) EXEC: coqproofworker.opt -main-channel stdfds -debug -worker-id proofworker:0 -async-proofs-worker-priority high
(Spawn  ,29770) PID 29775
[DEBUG] End of Coqide.main
[pid 29770] <-- Init None
[pid 29770] --> GOOD 1
29770:master:2] waiting for a task
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29770] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29770] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Feedback WorkerStatus
[DEBUG] selection_bound moved
got key '' (65507, )
got key '' (111, CONTROL)
[DEBUG] Loading file starts
[DEBUG] Loading: get raw content
[DEBUG] Loading: convert content
[DEBUG] Input is UTF-8
[DEBUG] Loading: create view
(Spawn  ,29765) EXEC: coqidetop.opt -main-channel stdfds --xml_format=Ppcmds -async-proofs on -topfile /home/pityhero/Documents/u2.v -debug
(Spawn  ,29765) PID 29784
[DEBUG] Start eval_call Init Some("/home/pityhero/Documents/u2.v")
[DEBUG] End eval_call
[DEBUG] Loading: stats
[DEBUG] Loading: fill buffer
[DEBUG] insert_cb 0
[DEBUG] target moved
[DEBUG] selection_bound moved
[DEBUG] Loading: success
(Spawn  ,29784) EXEC: coqproofworker.opt -main-channel stdfds -topfile /home/pityhero/Documents/u2.v -debug -worker-id proofworker:0 -async-proofs-worker-priority high
(Spawn  ,29784) PID 29788
29784:master:2] waiting for a task
[pid 29784] <-- Init Some("/home/pityhero/Documents/u2.v")
[pid 29784] --> GOOD 1
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Feedback Msg without a sentence Loading file /home/pityhero/Documents/.u2.aux: /home/pityhero/Documents/.u2.aux: No such file or directory
got key '' (65507, )
got key '' (65364, CONTROL)
[DEBUG] Begin command processing
[DEBUG] Start eval_call Add (("Inductive empty := .",-1),(1,true))
[DEBUG] End eval_call
[pid 29784] <-- Add (("Inductive empty := .",-1),(1,true))
[pid 29784] --> GOOD (2,(Inl ,""))
[DEBUG] Handling coqtop answer
[DEBUG] Marking  [ -1,  0](    0,   20) Inductive empty := . [P] 
[DEBUG] start_of_input moved
[DEBUG] selection_bound moved
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Goal 
[DEBUG] End eval_call
[pid 29784] <-- Goal 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Evars 
[DEBUG] End eval_call
[pid 29784] <-- Evars 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Status false
[DEBUG] End eval_call
[pid 29784] <-- Status false
[pid 29784] --> GOOD Status: path=u2;no proof;
[DEBUG] Handling coqtop answer
[DEBUG] Feedback ProcessingIn  on 2
[DEBUG] Marking  [ -1,  0](    0,   20) Inductive empty := . [P] 
[DEBUG] Feedback Msg empty is defined  on 2
[DEBUG] Feedback Msg empty_rect is defined  on 2
[DEBUG] Feedback Msg empty_ind is defined  on 2
[DEBUG] Feedback Msg empty_rec is defined  on 2
[DEBUG] Feedback Msg empty_sind is defined  on 2
[DEBUG] Feedback Processed  on 2
[DEBUG] Marking  [ -1,  0](    0,   20) Inductive empty := . [] 
[DEBUG] Feedback Processed  on 2
[DEBUG] Marking  [ -1,  0](    0,   20) Inductive empty := . [] 
[DEBUG] Feedback Processed  on 2
[DEBUG] Marking  [ -1,  0](    0,   20) Inductive empty := . [] 
got key '' (65364, CONTROL)
[DEBUG] Begin command processing
[DEBUG] Start eval_call Add (("\nInductive bool: Set := true | false.",-2),(2,true))
[DEBUG] End eval_call
[pid 29784] <-- Add (("\nInductive bool: Set := true | false.",-2),(2,true))
[pid 29784] --> GOOD (3,(Inl ,""))
[DEBUG] Handling coqtop answer
[DEBUG] Marking  [ -2,  0](   20,   57) Inductive bool: ... [P] 
[DEBUG] start_of_input moved
[DEBUG] selection_bound moved
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Goal 
[DEBUG] End eval_call
[pid 29784] <-- Goal 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Evars 
[DEBUG] End eval_call
[pid 29784] <-- Evars 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Status false
[DEBUG] End eval_call
[pid 29784] <-- Status false
[pid 29784] --> GOOD Status: path=u2;no proof;
[DEBUG] Handling coqtop answer
[DEBUG] Feedback ProcessingIn  on 3
[DEBUG] Marking  [ -2,  0](   20,   57) Inductive bool: ... [P] 
[DEBUG] Feedback Processed  on 2
[DEBUG] Marking  [ -1,  0](    0,   20) Inductive empty := . [] 
[DEBUG] Feedback Msg bool is defined  on 3
[DEBUG] Feedback Msg bool_rect is defined  on 3
[DEBUG] Feedback Msg bool_ind is defined  on 3
[DEBUG] Feedback Msg bool_rec is defined  on 3
[DEBUG] Feedback Msg bool_sind is defined  on 3
[DEBUG] Feedback Processed  on 3
[DEBUG] Marking  [ -2,  0](   20,   57) Inductive bool: ... [] 
[DEBUG] Feedback Processed  on 3
[DEBUG] Marking  [ -2,  0](   20,   57) Inductive bool: ... [] 
[DEBUG] Feedback Processed  on 3
[DEBUG] Marking  [ -2,  0](   20,   57) Inductive bool: ... [] 
got key '' (65364, CONTROL)
[DEBUG] Begin command processing
[DEBUG] Start eval_call Add (("\nDefinition negate (x: bool) :=\n  match x with\n  | true => false\n  | false => true\n  end.",-3),(3,true))
[DEBUG] End eval_call
[pid 29784] <-- Add (("\nDefinition negate (x: bool) :=\n  match x with\n  | true => false\n  | false => true\n  end.",-3),(3,true))
[pid 29784] --> GOOD (4,(Inl ,""))
[DEBUG] Handling coqtop answer
[DEBUG] Marking  [ -3,  0](   57,  146) Definition negat... [P] 
[DEBUG] start_of_input moved
[DEBUG] selection_bound moved
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Goal 
[DEBUG] End eval_call
[pid 29784] <-- Goal 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Evars 
[DEBUG] End eval_call
[pid 29784] <-- Evars 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Status false
[DEBUG] End eval_call
[pid 29784] <-- Status false
[pid 29784] --> GOOD Status: path=u2;no proof;
[DEBUG] Handling coqtop answer
got key '' (65364, CONTROL)
[DEBUG] Begin command processing
[DEBUG] Start eval_call Add (("\n\nCheck negate.",-4),(4,true))
[DEBUG] End eval_call
[pid 29784] <-- Add (("\n\nCheck negate.",-4),(4,true))
[pid 29784] --> GOOD (5,(Inl ,""))
[DEBUG] Handling coqtop answer
[DEBUG] Marking  [ -4,  0](  146,  161) Check negate. [P] 
[DEBUG] start_of_input moved
[DEBUG] selection_bound moved
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Goal 
[DEBUG] End eval_call
[pid 29784] <-- Goal 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Evars 
[DEBUG] End eval_call
[pid 29784] <-- Evars 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Status false
[DEBUG] End eval_call
[pid 29784] <-- Status false
[pid 29784] --> GOOD Status: path=u2;no proof;
[DEBUG] Handling coqtop answer
got key '' (65364, CONTROL)
[DEBUG] Begin command processing
[DEBUG] Start eval_call Add (("\n(* Natural Number is the set of either O or successor of natural number. *)\nInductive nat: Set := O: nat | S: nat -> nat.",-5),(5,true))
[DEBUG] End eval_call
[pid 29784] <-- Add (("\n(* Natural Number is the set of either O or successor of natural number. *)\nInductive nat: Set := O: nat | S: nat -> nat.",-5),(5,true))
[pid 29784] --> GOOD (6,(Inl ,""))
[DEBUG] Handling coqtop answer
[DEBUG] Marking  [ -5,  0](  161,  283) (* Natural Numbe... [P] 
[DEBUG] start_of_input moved
[DEBUG] selection_bound moved
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Goal 
[DEBUG] End eval_call
[pid 29784] <-- Goal 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Evars 
[DEBUG] End eval_call
[pid 29784] <-- Evars 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Status false
[DEBUG] End eval_call
[pid 29784] <-- Status false
[pid 29784] --> GOOD Status: path=u2;no proof;
[DEBUG] Handling coqtop answer
got key '' (65364, CONTROL)
[DEBUG] Begin command processing
[DEBUG] Start eval_call Add (("\nDefinition x := S (S (S O)).",-6),(6,true))
[DEBUG] End eval_call
[pid 29784] <-- Add (("\nDefinition x := S (S (S O)).",-6),(6,true))
[pid 29784] --> GOOD (7,(Inl ,""))
[DEBUG] Handling coqtop answer
[DEBUG] Marking  [ -6,  0](  283,  312) Definition x := ... [P] 
[DEBUG] start_of_input moved
[DEBUG] selection_bound moved
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Goal 
[DEBUG] End eval_call
[pid 29784] <-- Goal 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Evars 
[DEBUG] End eval_call
[pid 29784] <-- Evars 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Status false
[DEBUG] End eval_call
[pid 29784] <-- Status false
[pid 29784] --> GOOD Status: path=u2;no proof;
[DEBUG] Handling coqtop answer
got key '' (65364, CONTROL)
[DEBUG] Begin command processing
[DEBUG] Start eval_call Add (("\nPrint x.",-7),(7,true))
[DEBUG] End eval_call
[pid 29784] <-- Add (("\nPrint x.",-7),(7,true))
[pid 29784] --> GOOD (8,(Inl ,""))
[DEBUG] Handling coqtop answer
[DEBUG] Marking  [ -7,  0](  312,  321) Print x. [P] 
[DEBUG] start_of_input moved
[DEBUG] selection_bound moved
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Goal 
[DEBUG] End eval_call
[pid 29784] <-- Goal 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Evars 
[DEBUG] End eval_call
[pid 29784] <-- Evars 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Status false
[DEBUG] End eval_call
[pid 29784] <-- Status false
[pid 29784] --> GOOD Status: path=u2;no proof;
[DEBUG] Handling coqtop answer
got key '' (65364, CONTROL)
[DEBUG] Begin command processing
[DEBUG] Start eval_call Add (("\n(* Recursively define plus. *)\nFixpoint my_plus (u: nat) (v: nat) :=\n  match u with\n  | O => v\n  | S(u') => S(my_plus u' v)\n  end.",-8),(8,true))
[DEBUG] End eval_call
[pid 29784] <-- Add (("\n(* Recursively define plus. *)\nFixpoint my_plus (u: nat) (v: nat) :=\n  match u with\n  | O => v\n  | S(u') => S(my_plus u' v)\n  end.",-8),(8,true))
[pid 29784] --> GOOD (9,(Inl ,""))
[DEBUG] Handling coqtop answer
[DEBUG] Marking  [ -8,  0](  321,  452) (* Recursively d... [P] 
[DEBUG] start_of_input moved
[DEBUG] selection_bound moved
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Goal 
[DEBUG] End eval_call
[pid 29784] <-- Goal 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Evars 
[DEBUG] End eval_call
[pid 29784] <-- Evars 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Status false
[DEBUG] End eval_call
[pid 29784] <-- Status false
[pid 29784] --> GOOD Status: path=u2;no proof;
[DEBUG] Handling coqtop answer
got key '' (65364, CONTROL)
[DEBUG] Begin command processing
[DEBUG] Start eval_call Add (("\n\n\n\nCheck nat_rec.",-9),(9,true))
[DEBUG] End eval_call
[pid 29784] <-- Add (("\n\n\n\nCheck nat_rec.",-9),(9,true))
[pid 29784] --> GOOD (10,(Inl ,""))
[DEBUG] Handling coqtop answer
[DEBUG] Marking  [ -9,  0](  452,  470) Check nat_rec. [P] 
[DEBUG] start_of_input moved
[DEBUG] selection_bound moved
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Goal 
[DEBUG] End eval_call
[pid 29784] <-- Goal 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Evars 
[DEBUG] End eval_call
[pid 29784] <-- Evars 
[pid 29784] --> GOOD None
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Status false
[DEBUG] End eval_call
[pid 29784] <-- Status false
[pid 29784] --> GOOD Status: path=u2;no proof;
[DEBUG] Handling coqtop answer
got key '' (65364, CONTROL)
[DEBUG] Begin command processing
[DEBUG] Start eval_call Add (("\n\nCheck Set nat.",-10),(10,true))
[DEBUG] End eval_call
[pid 29784] <-- Add (("\n\nCheck Set nat.",-10),(10,true))
[pid 29784] --> GOOD (11,(Inl ,""))
[DEBUG] Handling coqtop answer
[DEBUG] Marking  [-10,  0](  470,  486) Check Set nat. [P] 
[DEBUG] start_of_input moved
[DEBUG] selection_bound moved
[DEBUG] Start eval_call SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[DEBUG] End eval_call
[pid 29784] <-- SetOptions [(["Diffs"],off);(["Printing";"Coercions"],false);(["Printing";"Matching"],true);(["Printing";"Notations"],true);(["Printing";"Existential";"Instances"],false);(["Printing";"Unfocused"],false);(["Printing";"Implicit"],false);(["Printing";"All"],false);(["Printing";"Universes"],false)]
[pid 29784] --> GOOD 
[DEBUG] Handling coqtop answer
[DEBUG] Start eval_call Goal 
[DEBUG] End eval_call
[pid 29784] <-- Goal 
[pid 29784] --> FAIL 10 (8,15)[Illegal application (Non-functional construction): 
The expression "Set" of type "Type"
cannot be applied to the term
 "nat" : "Set"
Raised at Exninfo.iraise in file "clib/exninfo.ml", line 80, characters 4-11
Called from Pretyping.Default.pretype_app in file "pretyping/pretyping.ml", line 868, characters 50-94
Called from Pretyping.pretype in file "pretyping/pretyping.ml" (inlined), line 1325, characters 2-81
Called from Pretyping.ise_pretype_gen in file "pretyping/pretyping.ml", line 1343, characters 21-79
Called from Pretyping.understand_tcc in file "pretyping/pretyping.ml", line 1391, characters 20-71
Called from Vernacentries.vernac_check_may_eval in file "vernac/vernacentries.ml", line 1711, characters 17-106
Called from Vernacentries.translate_vernac.(fun) in file "vernac/vernacentries.ml", line 2271, characters 8-43
Called from Vernacinterp.interp_typed_vernac in file "vernac/vernacinterp.ml", line 45, characters 4-13
Called from Vernacinterp.interp_control.(fun) in file "vernac/vernacinterp.ml", line 213, characters 24-64
Called from Flags.with_modified_ref in file "lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 82, characters 4-38
Called from Vernacinterp.interp_gen.(fun) in file "vernac/vernacinterp.ml", line 262, characters 18-43
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 260, characters 6-279
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 82, characters 4-38
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2153, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 956, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 82, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", line 2295, characters 4-105
Called from Stm.observe in file "stm/stm.ml", line 2477, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 82, characters 4-38
Called from Stm.finish in file "stm/stm.ml", line 2488, characters 12-50
Called from Idetop.goals in file "ide/coqide/idetop.ml", line 233, characters 13-28
Called from Idetop.eval_call.interruptible in file "ide/coqide/idetop.ml", line 456, characters 12-15
Called from Xmlprotocol.abstract_eval_call in file "ide/coqide/protocol/xmlprotocol.ml", line 683, characters 29-46
]
[DEBUG] Coqtop reader failed, resetting: Protocol violation. Expected: singleton Actual: list&nbsp;of&nbsp;length&nbsp;0
[DEBUG] Feedback ProcessingIn  on 4
[DEBUG] Marking  [ -3,  0](   57,  146) Definition negat... [P] 
[DEBUG] Feedback Processed  on 3
[DEBUG] Marking  [ -2,  0](   20,   57) Inductive bool: ... [] 
[DEBUG] Feedback Msg negate is defined  on 4
[DEBUG] Feedback Processed  on 4
[DEBUG] Marking  [ -3,  0](   57,  146) Definition negat... [] 
[DEBUG] Feedback Processed  on 4
[DEBUG] Marking  [ -3,  0](   57,  146) Definition negat... [] 
[DEBUG] Feedback Processed  on 4
[DEBUG] Marking  [ -3,  0](   57,  146) Definition negat... [] 
[DEBUG] Feedback ProcessingIn  on 5
[DEBUG] Marking  [ -4,  0](  146,  161) Check negate. [P] 
[DEBUG] Feedback Processed  on 4
[DEBUG] Marking  [ -3,  0](   57,  146) Definition negat... [] 
[DEBUG] Feedback Msg negate
             : bool -> bool  on 5
[DEBUG] Feedback Processed  on 5
[DEBUG] Marking  [ -4,  0](  146,  161) Check negate. [] 
[DEBUG] Feedback Processed  on 5
[DEBUG] Marking  [ -4,  0](  146,  161) Check negate. [] 
[DEBUG] Feedback Processed  on 5
[DEBUG] Marking  [ -4,  0](  146,  161) Check negate. [] 
[DEBUG] Feedback ProcessingIn  on 6
[DEBUG] Marking  [ -5,  0](  161,  283) (* Natural Numbe... [P] 
[DEBUG] Feedback Processed  on 5
[DEBUG] Marking  [ -4,  0](  146,  161) Check negate. [] 
[DEBUG] Feedback Msg nat is defined  on 6
[DEBUG] Feedback Msg nat_rect is defined  on 6
[DEBUG] Feedback Msg nat_ind is defined  on 6
[DEBUG] Feedback Msg nat_rec is defined  on 6
[DEBUG] Feedback Msg nat_sind is defined  on 6
[DEBUG] Feedback Processed  on 6
[DEBUG] Marking  [ -5,  0](  161,  283) (* Natural Numbe... [] 
[DEBUG] Feedback Processed  on 6
[DEBUG] Marking  [ -5,  0](  161,  283) (* Natural Numbe... [] 
[DEBUG] Feedback Processed  on 6
[DEBUG] Marking  [ -5,  0](  161,  283) (* Natural Numbe... [] 
[DEBUG] Feedback ProcessingIn  on 7
[DEBUG] Marking  [ -6,  0](  283,  312) Definition x := ... [P] 
[DEBUG] Feedback Processed  on 6
[DEBUG] Marking  [ -5,  0](  161,  283) (* Natural Numbe... [] 
[DEBUG] Feedback Msg x is defined  on 7
[DEBUG] Feedback Processed  on 7
[DEBUG] Marking  [ -6,  0](  283,  312) Definition x := ... [] 
[DEBUG] Feedback Processed  on 7
[DEBUG] Marking  [ -6,  0](  283,  312) Definition x := ... [] 
[DEBUG] Feedback Processed  on 7
[DEBUG] Marking  [ -6,  0](  283,  312) Definition x := ... [] 
[DEBUG] Feedback ProcessingIn  on 8
[DEBUG] Marking  [ -7,  0](  312,  321) Print x. [P] 
[DEBUG] Feedback Processed  on 7
[DEBUG] Marking  [ -6,  0](  283,  312) Definition x := ... [] 
[DEBUG] Feedback Msg x = S (S (S O))
                          : nat  on 8
[DEBUG] Feedback Processed  on 8
[DEBUG] Marking  [ -7,  0](  312,  321) Print x. [] 
[DEBUG] Feedback Processed  on 8
[DEBUG] Marking  [ -7,  0](  312,  321) Print x. [] 
[DEBUG] Feedback Processed  on 8
[DEBUG] Marking  [ -7,  0](  312,  321) Print x. [] 
[DEBUG] Feedback ProcessingIn  on 9
[DEBUG] Marking  [ -8,  0](  321,  452) (* Recursively d... [P] 
[DEBUG] Feedback Processed  on 8
[DEBUG] Marking  [ -7,  0](  312,  321) Print x. [] 
[DEBUG] Feedback Msg my_plus is defined  on 9
[DEBUG] Feedback Msg my_plus is recursively defined (guarded on 1st argument)
         on 9
[DEBUG] Feedback Processed  on 9
[DEBUG] Marking  [ -8,  0](  321,  452) (* Recursively d... [] 
[DEBUG] Feedback Processed  on 9
[DEBUG] Marking  [ -8,  0](  321,  452) (* Recursively d... [] 
[DEBUG] Feedback Processed  on 9
[DEBUG] Marking  [ -8,  0](  321,  452) (* Recursively d... [] 
[DEBUG] Feedback ProcessingIn  on 10
[DEBUG] Marking  [ -9,  0](  452,  470) Check nat_rec. [P] 
[DEBUG] Feedback Processed  on 9
[DEBUG] Marking  [ -8,  0](  321,  452) (* Recursively d... [] 
[DEBUG] Feedback Msg nat_rec
             : forall P : nat -> Set,
               P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
         on 10
[DEBUG] Feedback Processed  on 10
[DEBUG] Marking  [ -9,  0](  452,  470) Check nat_rec. [] 
[DEBUG] Feedback Processed  on 10
[DEBUG] Marking  [ -9,  0](  452,  470) Check nat_rec. [] 
[DEBUG] Feedback Processed  on 10
[DEBUG] Marking  [ -9,  0](  452,  470) Check nat_rec. [] 
[DEBUG] Feedback ProcessingIn  on 11
[DEBUG] Marking  [-10,  0](  470,  486) Check Set nat. [P] 
[DEBUG] Feedback Processed  on 10
[DEBUG] Marking  [ -9,  0](  452,  470) Check nat_rec. [] 
[pid 29784] Fatal exception in coqtop:
Stdlib.Sys.Break