https://gitlab.com/nomadic-labs/mi-cho-coq

sort by:
Revision Author Date Message Commit Date
eeb953e add contract_id 09 August 2019, 13:11:04 UTC
24410d2 [bloqued]instr type diff in diff module 09 August 2019, 10:13:52 UTC
825db89 creat Module merge_with_shared_storage 08 August 2019, 16:02:01 UTC
7022d11 [merge_example]add ContractContext 08 August 2019, 15:36:35 UTC
6723fc4 [contract_id] update .v 08 August 2019, 15:31:52 UTC
415524f add contract_id.v 08 August 2019, 14:53:27 UTC
d1e38fb fix semantic.v; projet compilable 02 August 2019, 14:54:12 UTC
16389e9 [cancelled_contract]running 02 August 2019, 14:47:56 UTC
1bcf7d5 [ifThenElse]mv to file 02 August 2019, 14:47:56 UTC
1f7dd90 close module 02 August 2019, 14:47:56 UTC
ee49514 code done 02 August 2019, 14:47:56 UTC
142ad57 [switch_to_pause]add spec 02 August 2019, 14:47:56 UTC
90bb39f [Contract_with_pause] add spec and compilator 02 August 2019, 14:47:56 UTC
8a4429f [Contract_resiliable.tz]improv clarety 02 August 2019, 14:47:56 UTC
0f09533 [pause_contract]add example Michelson 02 August 2019, 14:47:56 UTC
24feae2 [Contract_resiliable.tz] add squelette 02 August 2019, 14:47:56 UTC
99f0dcf [ifThenElse_code] clear code 02 August 2019, 14:47:56 UTC
d282668 [ifThenElse_code] done 02 August 2019, 14:47:56 UTC
8291b91 [IfThenElse.tz]done 02 August 2019, 14:47:56 UTC
1503fac [enable_pause_spec]compilable 02 August 2019, 14:47:56 UTC
a02ae33 [enable_pause_spec]en cours 02 August 2019, 14:47:56 UTC
73c4789 contract_with_pause_spec compilable 02 August 2019, 14:47:56 UTC
4d39131 [merge_with_shared_storage]add code and proof 02 August 2019, 14:47:56 UTC
96b0ea9 [semantic]add lemma fold_eval_precond 02 August 2019, 14:47:52 UTC
4246407 [util] add lemma split_imply 02 August 2019, 14:46:40 UTC
3ee4d0a [util]add ltac simpl_fuel 02 August 2019, 14:46:40 UTC
acafeb8 tmp 02 August 2019, 13:54:05 UTC
eb9dd1f lemma spec compilable 02 August 2019, 13:54:05 UTC
4d48302 facto 02 August 2019, 13:54:05 UTC
98e9ea5 new_contract pb solved 02 August 2019, 13:54:05 UTC
4105502 [question]how intros 02 August 2019, 13:54:05 UTC
e857b7b [question]order_instr typage 02 August 2019, 13:54:05 UTC
ee2d4c1 [question]((diff_1_ty,diff_2_ty) := order_storage diff_current_ty diff_other_ty ) 02 August 2019, 13:54:05 UTC
df30678 indent 02 August 2019, 13:54:04 UTC
9fc1d31 corrige error spec diff_other_final=diff_other_final 02 August 2019, 13:54:04 UTC
9c97c57 add destruct in eval_new_contract 02 August 2019, 13:54:04 UTC
ea3e37b add tactic eval_new_contract, tested ok 02 August 2019, 13:54:04 UTC
c78a48e [bloqued]merge contract other/current 02 August 2019, 13:54:04 UTC
1164866 abstract name case_inductive_correct 02 August 2019, 13:54:04 UTC
f44d0d1 add lemma cas_1_inductiv_correct, integred success 02 August 2019, 13:54:04 UTC
bd76416 solv error name in 2e branch 02 August 2019, 13:54:04 UTC
9c5ac5f rename,abstract b1_spec 02 August 2019, 13:54:03 UTC
61cb93b rename var b1_correct 02 August 2019, 13:54:03 UTC
87b5e07 correct b1_correct fuel error, b1_correct integred in proof 02 August 2019, 13:54:03 UTC
43a7ce1 tmp, 02 August 2019, 13:54:03 UTC
1e12b56 integre b1_spec in spec 02 August 2019, 13:54:03 UTC
b080289 clear b1_correct arg 02 August 2019, 13:54:03 UTC
781d119 b1_correct compilable 02 August 2019, 13:54:03 UTC
6a4879f tmp 02 August 2019, 13:54:03 UTC
3685c92 simpl spec branch1 ok 02 August 2019, 13:54:03 UTC
78b7570 add spec b1 02 August 2019, 13:54:02 UTC
f33ec8a ranger proof induction ok 02 August 2019, 13:54:02 UTC
1071190 simpl spec branch left compilable 02 August 2019, 13:54:02 UTC
b0fb009 insert merge_correct1 in merge_correct compilable 02 August 2019, 13:54:02 UTC
2188ce3 clear unless lemma 02 August 2019, 13:54:02 UTC
a51623e init file prototype 02 August 2019, 13:54:02 UTC
19f89de tmp 02 August 2019, 13:54:02 UTC
a08919d proof lemma of branch 02 August 2019, 13:54:01 UTC
7af74ac subst unless hyp 02 August 2019, 13:54:01 UTC
5a5c7b0 running 02 August 2019, 13:54:01 UTC
5d90520 [question]Unable to unify 02 August 2019, 13:54:01 UTC
9f6426f add lemma logique 02 August 2019, 13:54:01 UTC
c91b066 top down architecture 02 August 2019, 13:54:01 UTC
0d24179 add lemma proof exists of head 02 August 2019, 13:54:01 UTC
ff35bb8 rm unless ltac, definition 02 August 2019, 13:54:01 UTC
84a83fd compatible avec new version Michocoq 02 August 2019, 13:54:00 UTC
b0009e8 rm more_fuel ltac 02 August 2019, 13:54:00 UTC
36ff5e7 tmp save 02 August 2019, 13:54:00 UTC
07a3133 spec compilable 02 August 2019, 13:54:00 UTC
6141072 solv 1 pb in spec 02 August 2019, 13:54:00 UTC
6057cbe change contxt to module 02 August 2019, 13:54:00 UTC
568dcbf add untrack file 02 August 2019, 13:54:00 UTC
14c2e7b update spec "<-"; proof "<->" done 02 August 2019, 13:54:00 UTC
0027cd8 branch param2 comilable 02 August 2019, 13:54:00 UTC
28089fb clear branch comment; factorise in branch 02 August 2019, 13:53:59 UTC
c31f6cf 1 branch fini for <- lemma 02 August 2019, 13:53:59 UTC
6f4cfb7 [question]rewrite no find subterme 02 August 2019, 13:53:59 UTC
330c5a1 clear lemma comment 02 August 2019, 13:53:59 UTC
fe10748 proof -> done 02 August 2019, 13:53:59 UTC
9a9e2b2 fill spec for param2 02 August 2019, 13:53:59 UTC
9125109 proof done 1e branch 02 August 2019, 13:53:59 UTC
65d94b9 branch fini, a part parti admit 02 August 2019, 13:53:59 UTC
4cd5931 insert exists 02 August 2019, 13:53:58 UTC
bf5387c update spec nom 02 August 2019, 13:53:58 UTC
2c1aa09 proof head of spec done 02 August 2019, 13:53:58 UTC
03ca52e avancer in proof 02 August 2019, 13:53:58 UTC
0d890e3 new de correct 02 August 2019, 13:53:58 UTC
5ed5b8d lemma spec compilable 02 August 2019, 13:53:58 UTC
cde34da 1e spec branch spec compilable 02 August 2019, 13:53:58 UTC
ac23d2f clear spec, 02 August 2019, 13:53:58 UTC
14f4f1c merge for contract2 compilable 02 August 2019, 13:53:57 UTC
c447a4c branch contract1 compilable 02 August 2019, 13:53:57 UTC
f047f4a add merge-contract de autre branch in code 02 August 2019, 13:53:57 UTC
dc5352d add prototype code michelson 02 August 2019, 13:53:57 UTC
2bf9c94 fini redact spec 02 August 2019, 13:53:57 UTC
f2dae03 add spec debut 02 August 2019, 13:53:57 UTC
2c0bbbe rm inutil file 02 August 2019, 13:53:57 UTC
cc5c4ce adapter new version name 02 August 2019, 13:53:57 UTC
728e77d del comment 02 August 2019, 13:53:56 UTC
f8327e6 clear correct1 02 August 2019, 13:53:56 UTC
back to top