| 7cc81de | Pierre-Yves Strub | 01 December 2015, 15:29:19 UTC | .gitignore | 01 December 2015, 15:29:30 UTC |
| e6a3241 | Pierre-Yves Strub | 01 December 2015, 15:29:19 UTC | .gitignore | 01 December 2015, 15:29:19 UTC |
| e1b70b4 | Pierre-Yves Strub | 01 December 2015, 15:16:28 UTC | Pattern matching work modulo unfolding of locals. | 01 December 2015, 15:27:06 UTC |
| 214fcfc | Pierre-Yves Strub | 01 December 2015, 15:16:28 UTC | Pattern matching work modulo unfolding of locals. | 01 December 2015, 15:19:57 UTC |
| 1731c7e | Benjamin Gregoire | 01 December 2015, 14:55:01 UTC | improve error message: only monomorphic types are allowedt | 01 December 2015, 14:57:45 UTC |
| a09868d | Benjamin Gregoire | 01 December 2015, 14:55:01 UTC | improve error message: only monomorphic types are allowed | 01 December 2015, 14:55:11 UTC |
| ecaaf69 | Pierre-Yves Strub | 01 December 2015, 14:53:47 UTC | Exemplified new matching algo. | 01 December 2015, 14:54:52 UTC |
| 95a4b45 | Pierre-Yves Strub | 01 December 2015, 14:53:33 UTC | Better matching + matching always return a reduced subst. | 01 December 2015, 14:54:45 UTC |
| 6829f6b | Pierre-Yves Strub | 01 December 2015, 14:53:47 UTC | Exemplified new matching algo. | 01 December 2015, 14:53:47 UTC |
| 0db9002 | Pierre-Yves Strub | 01 December 2015, 14:53:33 UTC | Better matching + matching always return a reduced subst. | 01 December 2015, 14:53:33 UTC |
| df925d2 | Pierre-Yves Strub | 01 December 2015, 13:31:21 UTC | In proof-term, arguments can be partially constructed. As in: `apply (foo (x + _))` | 01 December 2015, 13:31:40 UTC |
| 7143ede | Pierre-Yves Strub | 01 December 2015, 13:31:21 UTC | In proof-term, arguments can be partially constructed. As in: `apply (foo (x + _))` | 01 December 2015, 13:31:21 UTC |
| 0fcb523 | Pierre-Yves Strub | 01 December 2015, 12:03:49 UTC | algebra: do not use t_fail internally. | 01 December 2015, 12:03:59 UTC |
| 3e4e3d0 | Pierre-Yves Strub | 01 December 2015, 12:03:49 UTC | algebra: do not use t_fail internally. | 01 December 2015, 12:03:49 UTC |
| f8aee22 | Pierre-Yves Strub | 01 December 2015, 11:50:02 UTC | More precise [proof-term checking / apply] error messages. | 01 December 2015, 11:50:02 UTC |
| 03f2eea | Pierre-Yves Strub | 01 December 2015, 11:41:53 UTC | More precise [proof-term checking / apply] error messages. | 01 December 2015, 11:41:53 UTC |
| b9ff6ff | Pierre-Yves Strub | 01 December 2015, 10:26:07 UTC | nits in Number (use proof terms) | 01 December 2015, 10:26:29 UTC |
| e15bc1d | Pierre-Yves Strub | 01 December 2015, 10:25:28 UTC | Do not fail on non-flat unification problems. | 01 December 2015, 10:26:29 UTC |
| 9d31264 | François Dupressoir | 01 December 2015, 09:49:49 UTC | FSet: some cleanup and extensions. | 01 December 2015, 10:26:28 UTC |
| 95b5ca7 | François Dupressoir | 01 December 2015, 09:49:35 UTC | Adding info to Vagrantfile on how to set emacs up. | 01 December 2015, 10:26:27 UTC |
| c9864c9 | Pierre-Yves Strub | 01 December 2015, 10:26:07 UTC | nits in Number (use proof terms) | 01 December 2015, 10:26:14 UTC |
| c12eb29 | Pierre-Yves Strub | 01 December 2015, 10:25:28 UTC | Do not fail on non-flat unification problems. | 01 December 2015, 10:26:14 UTC |
| be632c8 | François Dupressoir | 01 December 2015, 09:49:49 UTC | FSet: some cleanup and extensions. | 01 December 2015, 09:49:59 UTC |
| f184b17 | François Dupressoir | 01 December 2015, 09:49:35 UTC | Adding info to Vagrantfile on how to set emacs up. | 01 December 2015, 09:49:59 UTC |
| 2044e32 | Pierre-Yves Strub | 01 December 2015, 08:39:25 UTC | List: nth_rev. | 01 December 2015, 08:40:30 UTC |
| 09e0145 | Pierre-Yves Strub | 01 December 2015, 08:39:25 UTC | List: nth_rev. | 01 December 2015, 08:39:25 UTC |
| a12953c | Pierre-Yves Strub | 01 December 2015, 08:26:04 UTC | Importing some sha3 generic defs. | 01 December 2015, 08:26:51 UTC |
| c679271 | Pierre-Yves Strub | 01 December 2015, 08:26:04 UTC | Importing some sha3 generic defs. | 01 December 2015, 08:26:04 UTC |
| a0b80ad | Pierre-Yves Strub | 30 November 2015, 14:43:56 UTC | New rewrite construct: /#, /#= - /# stands for [smt ml=0] - /#= stands for [smt ml=0] + simplify. | 30 November 2015, 14:45:33 UTC |
| 24322f5 | Pierre-Yves Strub | 30 November 2015, 14:43:56 UTC | New rewrite construct: /#, /#= - /# stands for [smt ml=0] - /#= stands for [smt ml=0] + simplify. | 30 November 2015, 14:43:56 UTC |
| ccd708f | Pierre-Yves Strub | 30 November 2015, 14:12:55 UTC | Better check when overridding operators with type parameters. | 30 November 2015, 14:13:03 UTC |
| 6e53946 | Pierre-Yves Strub | 30 November 2015, 14:12:55 UTC | Better check when overridding operators with type parameters. | 30 November 2015, 14:12:55 UTC |
| b1404f2 | Pierre-Yves Strub | 30 November 2015, 13:07:13 UTC | Better infer. types for body of cloned operators/predicates. | 30 November 2015, 13:07:31 UTC |
| 81340be | Pierre-Yves Strub | 30 November 2015, 13:07:13 UTC | Better infer. types for body of cloned operators/predicates. | 30 November 2015, 13:07:13 UTC |
| 9843498 | Pierre-Yves Strub | 30 November 2015, 11:12:48 UTC | Parser/printer nits. - not bounded vars. are now printed as '_' - the syntax '_' is allowed for anonymous vars. - binders with several vars. with the same type can now be written as: `fun x y z : int => e` | 30 November 2015, 11:19:09 UTC |
| 54a39c6 | Pierre-Yves Strub | 30 November 2015, 11:12:48 UTC | Parser/printer nits. - not bounded vars. are now printed as '_' - the syntax '_' is allowed for anonymous vars. - binders with several vars. with the same type can now be written as: `fun x y z : int => e` | 30 November 2015, 11:12:48 UTC |
| 0a4653f | Pierre-Yves Strub | 30 November 2015, 08:45:32 UTC | Bits in BitWord + oflist/tolist. | 30 November 2015, 08:46:31 UTC |
| 2f59824 | Pierre-Yves Strub | 30 November 2015, 08:45:32 UTC | Bits in BitWord + oflist/tolist. | 30 November 2015, 08:45:32 UTC |
| c4f2b14 | Pierre-Yves Strub | 30 November 2015, 08:23:57 UTC | Import bits chunking from sha3 dev. | 30 November 2015, 08:24:10 UTC |
| 4d1eabc | Pierre-Yves Strub | 30 November 2015, 08:23:57 UTC | Import bits chunking from sha3 dev. | 30 November 2015, 08:23:57 UTC |
| 24c586c | Pierre-Yves Strub | 28 November 2015, 15:00:03 UTC | Nits. | 28 November 2015, 15:00:15 UTC |
| 5743b3a | Pierre-Yves Strub | 28 November 2015, 15:00:03 UTC | Nits. | 28 November 2015, 15:00:03 UTC |
| 0e96fcf | Pierre-Yves Strub | 28 November 2015, 13:53:59 UTC | List: before_find / before_index. | 28 November 2015, 13:54:08 UTC |
| cb30eba | Pierre-Yves Strub | 28 November 2015, 13:53:59 UTC | List: before_find / before_index. | 28 November 2015, 13:53:59 UTC |
| 67c363e | Pierre-Yves Strub | 27 November 2015, 15:39:42 UTC | In formulas, give priority to prog. vars over operators. | 27 November 2015, 15:40:00 UTC |
| e6aedae | Pierre-Yves Strub | 27 November 2015, 15:39:42 UTC | In formulas, give priority to prog. vars over operators. [fix #17274] | 27 November 2015, 15:39:42 UTC |
| ace7b84 | Pierre-Yves Strub | 27 November 2015, 13:55:39 UTC | Replug `transitivity` | 27 November 2015, 13:55:39 UTC |
| cfccd98 | Pierre-Yves Strub | 27 November 2015, 10:04:30 UTC | Proofs of cancelation of bs2int/int2bs. | 27 November 2015, 10:04:38 UTC |
| 08837a7 | Pierre-Yves Strub | 27 November 2015, 10:04:30 UTC | Proofs of cancelation of bs2int/int2bs. | 27 November 2015, 10:04:30 UTC |
| d31699b | Pierre-Yves Strub | 26 November 2015, 19:52:10 UTC | Some progress on summation. | 26 November 2015, 19:52:20 UTC |
| 795a33d | Pierre-Yves Strub | 26 November 2015, 19:52:10 UTC | Some progress on summation. | 26 November 2015, 19:52:10 UTC |
| e468348 | François Dupressoir | 26 November 2015, 17:02:53 UTC | A first Vagrant file. This one is for use in an active version of the repository. Commented lines in the provisioning script can be used to use OPAM for everything and distribute only the Vagrantfile. TODO: Give recipes and provisioning scripts for a wider variety of archs. | 26 November 2015, 19:44:01 UTC |
| b2e73f6 | François Dupressoir | 26 November 2015, 16:02:00 UTC | FSet: Some minor extensions. Need to make notations consistent throughout. | 26 November 2015, 19:44:00 UTC |
| f67e461 | François Dupressoir | 26 November 2015, 14:12:09 UTC | NewFMap: dom_set. | 26 November 2015, 19:43:58 UTC |
| cf83ecf | François Dupressoir | 26 November 2015, 17:02:53 UTC | A first Vagrant file. This one is for use in an active version of the repository. Commented lines in the provisioning script can be used to use OPAM for everything and distribute only the Vagrantfile. TODO: Give recipes and provisioning scripts for a wider variety of archs. | 26 November 2015, 17:02:53 UTC |
| 188b473 | François Dupressoir | 26 November 2015, 16:02:00 UTC | FSet: Some minor extensions. Need to make notations consistent throughout. | 26 November 2015, 16:02:08 UTC |
| 3dbaaf3 | François Dupressoir | 26 November 2015, 14:12:09 UTC | NewFMap: dom_set. | 26 November 2015, 16:02:08 UTC |
| 560f448 | Pierre-Yves Strub | 26 November 2015, 15:37:16 UTC | Nits on arithmetic && lists. | 26 November 2015, 15:37:55 UTC |
| e687477 | Pierre-Yves Strub | 26 November 2015, 15:37:16 UTC | Nits on arithmetic && lists. | 26 November 2015, 15:37:16 UTC |
| d05a093 | Pierre-Yves Strub | 25 November 2015, 15:29:24 UTC | Kill all admits in RealSeq. | 25 November 2015, 15:29:35 UTC |
| edccc8b | Pierre-Yves Strub | 25 November 2015, 15:29:13 UTC | Extend Number with RealField specific results. | 25 November 2015, 15:29:34 UTC |
| 0f2033d | Pierre-Yves Strub | 25 November 2015, 15:29:24 UTC | Kill all admits in RealSeq. | 25 November 2015, 15:29:24 UTC |
| 1ee53f9 | Pierre-Yves Strub | 25 November 2015, 15:29:13 UTC | Extend Number with RealField specific results. | 25 November 2015, 15:29:13 UTC |
| f3fb324 | François Dupressoir | 25 November 2015, 14:38:04 UTC | fix smt in DList. | 25 November 2015, 14:40:56 UTC |
| 75690fb | François Dupressoir | 25 November 2015, 14:16:11 UTC | fix smt in NewFMap. | 25 November 2015, 14:40:55 UTC |
| e4dd849 | François Dupressoir | 25 November 2015, 14:07:35 UTC | fix smt in List. | 25 November 2015, 14:40:52 UTC |
| 4e9daae | François Dupressoir | 25 November 2015, 14:38:04 UTC | fix smt in DList. | 25 November 2015, 14:38:26 UTC |
| 19a83cd | François Dupressoir | 25 November 2015, 14:16:11 UTC | fix smt in NewFMap. | 25 November 2015, 14:38:26 UTC |
| 1860966 | François Dupressoir | 25 November 2015, 14:07:35 UTC | fix smt in List. | 25 November 2015, 14:38:26 UTC |
| 098dfb0 | Pierre-Yves Strub | 25 November 2015, 11:11:19 UTC | Progressing on countable summation, reducing all admits to ppties on limits. The lub operator has been pushed into its own theory. | 25 November 2015, 11:11:30 UTC |
| ffe0d4f | Pierre-Yves Strub | 25 November 2015, 11:10:35 UTC | More on pmap + link between map/nth/range. | 25 November 2015, 11:11:29 UTC |
| 28217e7 | Pierre-Yves Strub | 25 November 2015, 11:11:19 UTC | Progressing on countable summation, reducing all admits to ppties on limits. The lub operator has been pushed into its own theory. | 25 November 2015, 11:11:19 UTC |
| 2c0495c | Pierre-Yves Strub | 25 November 2015, 11:10:35 UTC | More on pmap + link between map/nth/range. | 25 November 2015, 11:10:35 UTC |
| 5bc7419 | François Dupressoir | 25 November 2015, 10:40:13 UTC | Word: rewrite as a refinement of arrays. | 25 November 2015, 11:06:55 UTC |
| ec412c2 | François Dupressoir | 25 November 2015, 10:39:00 UTC | NewLogic: comment out overloadings of && and ||. At the moment, the theory cannot be imported without causing issues. | 25 November 2015, 11:06:54 UTC |
| 3124db7 | François Dupressoir | 25 November 2015, 10:40:13 UTC | Word: rewrite as a refinement of arrays. | 25 November 2015, 10:57:49 UTC |
| 4ba22d6 | François Dupressoir | 25 November 2015, 10:39:00 UTC | NewLogic: comment out overloadings of && and ||. At the moment, the theory cannot be imported without causing issues. | 25 November 2015, 10:39:00 UTC |
| 8f4435c | François Dupressoir | 25 November 2015, 10:12:14 UTC | NewLogic: Equivalences of quantified statements. | 25 November 2015, 10:14:40 UTC |
| 0309ff2 | François Dupressoir | 25 November 2015, 10:12:14 UTC | NewLogic: Equivalences of quantified statements. | 25 November 2015, 10:12:32 UTC |
| b57d8a5 | Benjamin Gregoire | 25 November 2015, 09:27:53 UTC | fix printing of lvalue in program : x[e] ---> x.[e] | 25 November 2015, 09:45:22 UTC |
| 445ce13 | Benjamin Gregoire | 25 November 2015, 09:27:53 UTC | fix printing of lvalue in program : x[e] ---> x.[e] | 25 November 2015, 09:27:53 UTC |
| b57ee16 | Pierre-Yves Strub | 24 November 2015, 21:48:29 UTC | Pushing current status on real seq/series. | 24 November 2015, 21:48:38 UTC |
| dfdf69a | Pierre-Yves Strub | 24 November 2015, 21:48:29 UTC | Pushing current status on real seq/series. | 24 November 2015, 21:48:29 UTC |
| dc6856e | Pierre-Yves Strub | 24 November 2015, 21:00:46 UTC | Fix BitEncoding proofs. | 24 November 2015, 21:01:36 UTC |
| d25415a | François Dupressoir | 24 November 2015, 20:38:59 UTC | Fixing Matrix. Removing Array import from RealSeq. | 24 November 2015, 21:01:35 UTC |
| 22e2b9c | Pierre-Yves Strub | 24 November 2015, 21:00:46 UTC | Fix BitEncoding proofs. | 24 November 2015, 21:01:14 UTC |
| 323df28 | François Dupressoir | 24 November 2015, 20:38:59 UTC | Fixing Matrix. Removing Array import from RealSeq. | 24 November 2015, 20:39:38 UTC |
| 9b3d27b | François Dupressoir | 24 November 2015, 16:05:42 UTC | Clean Array theory. Word should be based off of this with fixed length and base type. | 24 November 2015, 20:06:23 UTC |
| a334b84 | Pierre-Yves Strub | 24 November 2015, 20:05:43 UTC | runtest: when in recursive mode, scan also the root directory. | 24 November 2015, 20:06:20 UTC |
| 6fe3ab2 | Pierre-Yves Strub | 24 November 2015, 20:05:43 UTC | runtest: when in recursive mode, scan also the root directory. | 24 November 2015, 20:06:03 UTC |
| 3e2b813 | François Dupressoir | 24 November 2015, 16:05:42 UTC | Clean Array theory. Word should be based off of this with fixed length and base type. | 24 November 2015, 16:05:50 UTC |
| e73c89e | Pierre-Yves Strub | 24 November 2015, 13:36:03 UTC | More results on bigops. | 24 November 2015, 13:36:26 UTC |
| 7141c60 | Pierre-Yves Strub | 24 November 2015, 13:36:03 UTC | More results on bigops. | 24 November 2015, 13:36:03 UTC |
| b953aef | Benjamin Gregoire | 24 November 2015, 12:50:08 UTC | fix syntax | 24 November 2015, 12:50:08 UTC |
| 6623704 | Pierre-Yves Strub | 24 November 2015, 12:29:11 UTC | More on divisibility and ordering. | 24 November 2015, 12:29:36 UTC |
| 5fbe3f0 | Pierre-Yves Strub | 24 November 2015, 12:29:11 UTC | More on divisibility and ordering. | 24 November 2015, 12:29:11 UTC |
| d6c87af | Pierre-Yves Strub | 24 November 2015, 11:36:02 UTC | Start to generalize and incorporates some ad-hoc lemmas of IntDiv. | 24 November 2015, 11:36:19 UTC |
| a9c5810 | Pierre-Yves Strub | 24 November 2015, 11:36:02 UTC | Start to generalize and incorporates some ad-hoc lemmas of IntDiv. | 24 November 2015, 11:36:02 UTC |
| b0dffaf | Pierre-Yves Strub | 24 November 2015, 10:28:15 UTC | Integer divisibility def. + core ppties. | 24 November 2015, 10:28:35 UTC |
| d9d5e00 | Pierre-Yves Strub | 24 November 2015, 10:27:58 UTC | Change ops. priority. Operators of the form %+(.) has the priority of \1. | 24 November 2015, 10:28:34 UTC |
