Commit 25acc03a authored by MARCHE Claude's avatar MARCHE Claude

fix issue #85

The naming is now "consistent" in the sense that a transformation
argument is not taken in place of another.

However, it does not solve all the issues related to using
the IDE without the "introduce premises" enabled.
parent 95edf23e
......@@ -881,12 +881,10 @@ end
(* -- send the task -- *)
let task_of_id d id do_intros show_full_context loc =
let task,tables =
if do_intros then get_task d.cont.controller_session id
let task = get_raw_task d.cont.controller_session id in
let tables = Args_wrapper.build_naming_tables task in
let task,tables = get_task d.cont.controller_session id in
let task =
if do_intros then task else
get_raw_task d.cont.controller_session id
(* This function also send source locations associated to the task *)
let loc_color_list = if loc then get_locations task else [] in
module Naming
use import int.Int
constant x : int
goal G : forall x:int. x >= 0 -> x = 0
module ApplyRewrite
......@@ -10,6 +10,10 @@
<prover id="5" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../demo-itp.mlw">
<theory name="Naming" sum="887148d0be0266efa5001ad2fedbe72e">
<goal name="G">
<theory name="ApplyRewrite" sum="a5d903eba2570fb4645483c4ff500ebb">
<goal name="g1" proved="true">
<transf name="apply" proved="true" arg1="H">
......@@ -46,7 +50,7 @@
<goal name="gb">
<theory name="Soundness" sum="198ba2949deb2335512120811dfebfc6">
<theory name="Soundness" sum="aa1c41b51a76f536179c52b8dcf8a473">
<goal name="A" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.24"/></proof>
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment